proposition: Lemma integer_induction1 h a p: natp p -> exists! f, [/\ source f = Nat, surjection f, Vf f \0c = a , (forall n, n <c p -> Vf f (csucc n) = h n (Vf f n)) & (forall n, natp n -> ~ (n <=c p) -> Vf f n = a)].
proof: Proof. move=> pN; exists (induction_defined1 h a p); split. by apply: induction_defined_pr1. have [sx sjx x0 xs xl] := (induction_defined_pr1 h a pN). move => y [sy sjy y0 ys yl]. apply function_exten4=>//; first by ue. rewrite sx; apply: Nat_induction; first by ue. move=> n nN eq. case: (p_or_not_p (n <c p)) => np. by rewrite (xs _ np) (ys _ np) eq. have snp: (~ (csucc n) <=c p) by move /cleSltP; fprops. have snN:= (NS_succ nN). by rewrite (xl _ snN snp) (yl _ snN snp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)