(**************************************************************************)
include "ground_2/ynat/ynat_max.ma".
-include "basic_2/computation/lsx_ldrop.ma".
+include "basic_2/computation/lsx_drop.ma".
include "basic_2/computation/lsx_lpx.ma".
include "basic_2/computation/lsx_lpxs.ma".
include "basic_2/computation/lcosx.ma".
[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #d #HL #H
elim (ylt_split i d) #Hdi [ -H | -HL ]
[ <(ymax_pre_sn d (⫯i)) /2 width=1 by ylt_fwd_le_succ/
- elim (lcosx_ldrop_trans_lt … HL … HLK) // -HL -Hdi
- lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/
+ elim (lcosx_drop_trans_lt … HL … HLK) // -HL -Hdi
+ lapply (drop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/
| lapply (lsx_fwd_lref_be … H … HLK) // -H -Hdi
- lapply (ldrop_fwd_drop2 … HLK) -HLK
+ lapply (drop_fwd_drop2 … HLK) -HLK
/4 width=10 by lsx_ge, lsx_lift_le/
]
| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H
elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/
| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #d #HL #H
elim (lsx_inv_bind … H) -H
- /4 width=9 by lcosx_pair, lsx_inv_lift_ge, ldrop_drop/
+ /4 width=9 by lcosx_pair, lsx_inv_lift_ge, drop_drop/
| #G #L #V #T1 #T2 #_ #IHT12 #d #HL #H
elim (lsx_inv_flat … H) -H /2 width=1 by/
| #G #L #V1 #V2 #T #_ #IHV12 #d #HL #H
elim (lsx_inv_flat … H) -H #HV1 #H
elim (lsx_inv_bind … H) -H #HW1 #HT1
@lsx_bind /2 width=1 by/ (**) (* explicit constructor *)
- @lsx_flat [ /3 width=7 by lsx_lift_ge, ldrop_drop/ ]
+ @lsx_flat [ /3 width=7 by lsx_lift_ge, drop_drop/ ]
@(lsx_leq_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, leq_succ/
]
qed-.