proposition: Lemma integer_induction_stable0 E h a: inc a E -> (forall n x, inc x E -> natp n -> inc (h n x) E) -> sub (target (induction_defined0 h a)) E.
proof: Proof. move=> aE ahE t tt. have [sf sjf f0 fn] := (induction_defined_pr0 h a). have [x xsf ->] :=(proj2 sjf _ tt). move: x xsf;rewrite sf;apply: Nat_induction; first by ue. by move=> n nN WE; rewrite fn //; apply: ahE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)