proposition: Lemma ex6_fct_fi: injection ex6_iso.
proof: Proof. apply:(lf_injective ex6_fct_ax). rewrite /ex6_fct;move => x x' /ex6_F_prop1. set j := Q _; set i := Q _; set y := P _; move =>[jL iJl yE ->]. move /ex6_F_prop1;set j' := Q _; set i' := Q _; set y' := P _. move =>[jL' iJl' yE' ->]. move: (ex6_prop1 jL iJl)(ex6_prop1 jL' iJl'); rewrite ex6_prop3 => iI iI'. move/(inl_class_eq_bis iI iI' yE yE') => [i'' []]; aw => le1 le2 eq1. move:(arg2_sr le1); rewrite rS HIs - HJI => /setUb_P [j2]; rewrite HJd. move => j2L iJl2. move:(HLd jL jL') => [j3 [j3L lea leb]]. move:(HLd j2L j3L) => [j4 [j4L lec led]]. move:(proj33 HLp _ _ _ lea led)(proj33 HLp _ _ _ leb led) => lejj4 lejj4'. rewrite(ex6_F_prop2 iJl yE lejj4) (ex6_F_prop2 iJl' yE' lejj4'). move:(HJm lejj4 iJl) (HJm lejj4' iJl') => iJl4 iJl4'. have yE4: inc y (Vg (restr (isE S) (Vg Jf j4)) i) by rewrite LgV. have yE4': inc y' (Vg (restr (isE S) (Vg Jf j4)) i') by rewrite LgV. have leii'': gle (induced_order (isr S) (Vg Jf j4)) i i''. by apply/iorder_gle0P => //; apply (HJm lec iJl2). have lei'i'': gle (induced_order (isr S) (Vg Jf j4)) i' i''. by apply/iorder_gle0P => //; apply (HJm lec iJl2). rewrite /ex6_F_val; congr (class _ (J _ j4)). rewrite (ex6_prop6a j4L); apply/inl_class_eq_bis => //. exists i''; aw;split => //=; rewrite !LgV //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)