proposition: Lemma ex4_inF_hi x (n := domain x): inc x ex4_F -> [/\ n <> \0c, ex4_seqp x n & forall i, i<c n -> pairp (Vg x i)].
proof: Proof. move/Zo_P => [ha [m mp hu]]; move: (hu)=> [hb hc hd _ _]. move/sub_fgraphsP: (ha) => [C CN /gfunctions_P2 [_ _ xr]]. rewrite /n hd; split => // i /(NltP hb) lim. have: inc (Vg x i) (range x) by apply/(range_gP hc); exists i => //; ue. by move/xr => /setX_P []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)