proposition: Lemma ex4_inF x n : n <> \0c -> ex4_seqp x n -> (forall i, i<c n -> pairp (Vg x i)) -> inc x ex4_F.
proof: Proof. move => ha hb hc. move: (hb)=> [q1 q2 q3 q4 q5]; apply/Zo_P; split => //; last by exists n. apply/sub_fgraphsP; exists n;first by move => t tn; move:(NS_inc_nat q1 tn). apply/gfunctions_P2; split => // t /(range_gP q2) [j jdx ->]. move: jdx; rewrite q3 => /(NltP q1) => ljn. move:(proj1(q4 _ ljn)) => lij; move:(ex4_or_prop0 lij) => [p1 p2]. by move:(hc _ ljn) =>p3;apply/setX_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)