(*#* #caption "transitivity, second case" *)
(*#* #cap #alpha c1 in C1, c2 in C, e2 in C2, d in i, i in k *)
Theorem drop_trans_ge : (i:?; c1,c2:?; d,h:?) (drop h d c1 c2) ->
(e2:?) (drop i (0) c2 e2) -> (le d i) ->
(drop (plus i h) (0) c1 e2).
(*#* #caption "transitivity, second case" *)
(*#* #cap #alpha c1 in C1, c2 in C, e2 in C2, d in i, i in k *)
Theorem drop_trans_ge : (i:?; c1,c2:?; d,h:?) (drop h d c1 c2) ->
(e2:?) (drop i (0) c2 e2) -> (le d i) ->
(drop (plus i h) (0) c1 e2).