proposition: Lemma ex4_F_special i: inc i I -> exists2 x, inc x ex4_F & ex4_fct_r x = i.
proof: Proof. move => iI. move:(ex4_no_greater iI) => [j lij]. set x := Lg \1c (fun z => J i j). have fgx: fgraph x by rewrite /x; fprops. have dx: domain x = \1c by rewrite /x; aw. have ha: ex4_fct_r x = i. by rewrite/ex4_fct_r /ex4_last dx cpred1 /x LgV//; aw;trivial;apply:set1_1. have hb:forall k, k <c \1c -> pairp (Vg x k). rewrite /x; move=> k /(NltP NS1) kk; rewrite LgV//; fprops. exists x => //;apply:(ex4_inF card1_nz _ hb); split; fprops. by rewrite /x;move => t /(NltP NS1) kk; rewrite LgV//;aw. by move => a b lab /clt1 bz; move: lab; rewrite bz => /clt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)