proposition: Lemma integer_induction_stable E g a: inc a E -> (forall x, inc x E -> inc (g x) E) -> sub (target (induction_defined g a)) E.
proof: Proof. move=> eA agE t tt. have [sf sjf f0 fn]:=(induction_defined_pr g 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: agE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)