-| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt
- lapply (transitive_le … Hdedt … Hdti) #Hdei
- elim (le_inv_plus_l … Hdedt) -Hdedt #_ #Hedt
- elim (le_inv_plus_l … Hdei) #Hdie #Hei
- lapply (lift_inv_lref2_ge … H … Hdei) -H #H destruct
- lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV
- elim (lift_split … HVW d (i-e+1)) -HVW [2,3,4: /2 width=1 by le_S_S, le_S/ ] -Hdei -Hdie
- #V0 #HV10 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O #H
- @(ex2_intro … H) @(cpy_subst … HKV HV10) /2 width=1 by monotonic_le_minus_l2/ (**) (* explicit constructor *)
- >plus_minus /2 width=1 by monotonic_lt_minus_l/
-| #a #I #G #L #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
- elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
- elim (le_inv_plus_l … Hdetd) #_ #Hedt
- elim (IHV12 … HLK … HWV1) -V1 // #W2 #HW12 #HWV2
- elim (IHU12 … HTU1) -U1 [4: @ldrop_skip // |2: skip |3: /2 width=1 by le_S_S/ ]
- <plus_minus /3 width=5 by cpy_bind, lift_bind, ex2_intro/
-| #I #G #L #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
- elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
- elim (IHV12 … HLK … HWV1) -V1 //
+| #I #G #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #s #d #e #HLK #T1 #H #Hdedt
+ lapply (yle_trans … Hdedt … Hdti) #Hdei
+ elim (yle_inv_plus_inj2 … Hdedt) -Hdedt #_ #Hedt
+ elim (yle_inv_plus_inj2 … Hdei) #Hdie #Hei
+ lapply (lift_inv_lref2_ge … H ?) -H /2 width=1 by yle_inv_inj/ #H destruct
+ lapply (ldrop_conf_ge … HLK … HLKV ?) -L /2 width=1 by yle_inv_inj/ #HKV
+ elim (lift_split … HVW d (i-e+1)) -HVW [2,3,4: /3 width=1 by yle_inv_inj, le_S_S, le_S/ ] -Hdei -Hdie
+ #V0 #HV10 >plus_minus /2 width=1 by yle_inv_inj/ <minus_minus /3 width=1 by yle_inv_inj, le_S/ <minus_n_n <plus_n_O #H
+ @(ex2_intro … H) @(cpy_subst … HKV HV10) (**) (* explicit constructor *)
+ [ /2 width=1 by monotonic_yle_minus_dx/
+ | <yplus_minus_comm_inj /2 width=1 by monotonic_ylt_minus_dx/
+ ]
+| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
+ elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
+ elim (yle_inv_plus_inj2 … Hdetd) #_ #Hedt
+ elim (IHW12 … HLK … HVW1) -IHW12 // #V2 #HV12 #HVW2
+ elim (IHU12 … HTU1) -U1 [4: @ldrop_skip // |2,5: skip |3: /2 width=1 by yle_succ/ ]
+ >yminus_succ1_inj /3 width=5 by cpy_bind, lift_bind, ex2_intro/
+| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
+ elim (lift_inv_flat2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
+ elim (IHW12 … HLK … HVW1) -W1 //