proposition: Lemma induction_defined_pr0 (h:fterm2) a (f := induction_defined0 h a): [/\ source f = Nat, surjection f, Vf f \0c = a & forall n, natp n -> Vf f (csucc n) = h n (Vf f n)].
proof: Proof. rewrite /f /induction_defined0. set p := (fun u : Set => _). have [wo sr] := Nat_order_wor. move: (transfinite_defined_pr p wo) => []. set g := (transfinite_defined Nat_order p) => pa pb pc. have p1: forall a, natp a -> source (restriction1 f (segment Nat_order a))= a. by move=> b bN; rewrite /restriction1 corresp_s segment_Nat_order1. rewrite sr in pb pc; split => //. by rewrite (pc _ NS0) /p (p1 _ NS0) variant_true0. move=> n nN; move:(NS_succ nN) => snN;rewrite (pc _ snN) /p (p1 _ snN). rewrite (variant_false _ _ (@succ_nz n)) (cpred_pr2 nN). congr (h n _); rewrite restriction1_V //; first by fct_tac. rewrite segment_Nat_order // ? pb;apply: Nint_S1. by rewrite (segment_Nat_order snN); apply: Nint_si. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)