proposition: Lemma ex4_function_f_sf a b:gle r a b -> surjection (ex4_function_f (J a b)).
proof: Proof. move => leab. move:ex4H => [_ or sr _ _]. move: (arg1_sr leab) (arg2_sr leab); rewrite sr => aI bI. case: (equal_or_not a b) => eqab. by rewrite eqab (ex4_function_f_id bI); case: (identity_fb (ex4_setEi b)). apply: lf_surjective; first by apply: ex4_function_f_ax; aw. aw; move => y /Zo_P [yF yr]. move:(ex4_length_prop1 yF) => [sa sb]. move/ex4_inF_hi:yF =>[y1 [nN y3 y4 y5 y6] y7]. set n := domain y. move:(ex4_no_greater bI) => [c cI]. pose x := Lg (csucc n) (fun z => Yo (z <c n) (Vg y z) (J b c)). have dx: domain x = csucc n by rewrite /x Lgd. have lenn:= (cleS nN). have snN:= (NS_succ nN). have xv_in i: i <c n -> Vg x i = Vg y i. move => iN; rewrite /x LgV//; first by Ytac0. apply/(NltP snN); apply: (clt_leT iN lenn). have xv_out: Vg x n = (J b c). rewrite/x LgV//; first by rewrite Y_false //; case. apply/(NltP snN); exact:(cltS nN). have fgx: fgraph x by rewrite /x; fprops. have hu: ex4_last y <c n by rewrite /n sb; apply:cltS. have dxnz:= (@succ_nz n). have xF: inc x (ex4_F). have pa i: i <c csucc n -> pairp (Vg x i). move/(cltSleP nN);case/cle_eqVlt => lt;first by rewrite lt xv_out; fprops. by rewrite (xv_in _ lt); apply: y7. apply/(ex4_inF dxnz _ pa); split => //. move => i/(cltSleP nN);case/cle_eqVlt => lt; first by rewrite lt xv_out; aw. by rewrite (xv_in _ lt); apply: y5. move => i j lji /(cltSleP nN) lein. rewrite (xv_in _ (clt_leT lji lein)); case/cle_eqVlt:lein => lt; last first. by rewrite (xv_in _ lt); apply: y6. rewrite lt xv_out pr1_pair => lebv. have ltab: glt r a b by split. have laij: glt r a (P (Vg y j)) by order_tac. case: (equal_or_not j (ex4_last y)) => jv. by case: (proj2 laij); rewrite - yr jv. have hv: j <c ex4_last y by split=> //;apply/(cltSleP sa); rewrite - sb -lt. move:(y6 (ex4_last y) j hv hu); case; rewrite -/(ex4_fct_r y) yr. exact: proj1 laij. have xr: ex4_fct_r x = b. by rewrite /ex4_fct_r {2}/x /ex4_last Lgd (cpred_pr2 nN) xv_out; aw. have xe: inc x (ex4_setEi b) by apply /Zo_P. exists x => //. have leaxv: gle r a (ex4_fct_r x) by rewrite xr. case:(ex4_indexj_correct xF leaxv). set d := ex4_indexj x a; rewrite dx; move/(cltSleP nN) => dp1 dp2 dp3. have ha: (ex4_last y) <c csucc n by apply: (clt_leT hu (cleS nN)). case: (NleT_ell (NS_le_nat dp1 nN) sa); last first. case/cltNge; apply:(dp3 _ ha). by rewrite (xv_in _ hu) -/(ex4_fct_r y) yr; order_tac; rewrite sr. move => lt1. case: (y6 (ex4_last y) d lt1 hu); rewrite -/(ex4_fct_r y) yr - (xv_in) //. apply: (clt_ltT lt1 hu). move => dv. rewrite /ex4_function_fv -/d dv - sb /ex4_modify_r /ex4_last restr_d. apply: fgraph_exten;[done | fprops| by aw | move => i idg /=; rewrite LgV //LgV//]. move/(NltP nN): idg => lin. rewrite (xv_in _ lin); Ytac eqa => //. by rewrite - yr /ex4_fct_r /ex4_last - eqa y7. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)