DEFINITION drop_trans_ge()
TYPE =
       ∀i:nat
         .∀c1:C
           .∀c2:C
             .∀d:nat
               .∀h:nat
                 .drop h d c1 c2
                   →∀e2:C.(drop i O c2 e2)→(le d i)→(drop (plus i h) O c1 e2)
BODY =
Show proof