DEFINITION drop_conf_ge()
TYPE =
       ∀i:nat
         .∀a:C
           .∀c:C
             .drop i O c a
               →∀e:C
                    .∀h:nat
                      .∀d:nat
                        .drop h d c e
                          →(le (plus d h) i)→(drop (minus i h) O e a)
BODY =
Show proof