proposition: Lemma ex4_F_stable_restr x m: inc x ex4_F -> m <=c domain x -> m <> \0c -> inc (restr x m) ex4_F.
proof: Proof. move/ex4_inF_hi => [h1 [h2 h3 _ h5 h6 ] h7] pa pb. have mN := NS_le_nat pa h2. have ra i: i <c m -> (Vg (restr x m) i) = Vg x i. by move => lim;rewrite LgV//; apply/(NltP mN). have rb i: i <c m -> pairp (Vg (restr x m) i). move => lim; rewrite (ra _ lim); apply: (h7 _ (clt_leT lim pa)). apply:(ex4_inF pb _ rb); split => //. - fprops. - by aw. - move => i lim; rewrite (ra _ lim); apply: (h5 _ (clt_leT lim pa)). - move => i j lji lim; rewrite (ra _ lim) (ra _ (clt_ltT lji lim)). apply:(h6 _ _ lji (clt_leT lim pa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)