proposition: Lemma induction_defined_pr_set E g a (f := induction_defined_set g a E): inc a E -> (forall x, inc x E -> inc (g x) E) -> [/\ function_prop f Nat E, Vf f \0c = a & forall n, natp n -> Vf f (csucc n) = g (Vf f n)].
proof: Proof. move => aE ag. have st:= (integer_induction_stable aE ag). have [sf [ff _] f0 fs] := (induction_defined_pr g a). move: (change_target_pr ff st); rewrite -/(induction_defined_set g a E) -/f. rewrite sf; move => [pa pd]. split => //; first by rewrite -f0 pd //; exact: NS0. by move => n nb; rewrite (pd _ (NS_succ nb)) (fs _ nb) -pd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)