proposition: Lemma integer_induction0 h a: exists! f, [/\ source f = Nat, surjection f, Vf f \0c = a & forall n, natp n -> Vf f (csucc n) = h n (Vf f n)].
proof: Proof. exists (induction_defined0 h a); split. apply: (induction_defined_pr0). move:(induction_defined_pr0 h a) => [sy sjy y0 ys] x [sx sjx x0 xs]. apply: function_exten4=>//; first by ue. rewrite sy; apply: Nat_induction; first by ue. by move=> n nN eq; rewrite (xs _ nN) (ys _ nN) eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)