proposition: Lemma nds_induction_prop a b T (f := nds_induction a b T) : [/\ Vf f \0c = a, Vf f \1c = b & forall n, natp n -> \1c <c n -> Vf f n = T (nds_k_of n) (Vf f (n -c (nds_k_of n)))].
proof: Proof. rewrite /f/nds_induction. 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=> c cN; rewrite /restriction1 corresp_s segment_Nat_order1. rewrite sr in pb pc; split. - by rewrite (pc _ NS0) /p (p1 _ NS0); Ytac0. - rewrite (pc _ NS1) /p (p1 _ NS1); Ytac0; rewrite (Y_false); fprops. - move => n nN ln2; rewrite (pc _ nN) /p (p1 _ nN). move: (nesym (proj2 ln2)) => nn1. have nn0: n <> \0c by move => bad; move: ln2; rewrite bad => /clt0. move:(nds_k_of_bd nN ln2) => [qa qb]. have qc: inc (n -c nds_k_of n) n. apply/(NltP nN); apply: (cdiff_ltb nN (proj1 qb) (nesym (proj2 qa))). have sng: sub n (source g) by rewrite pb; exact :(NS_inc_nat nN). Ytac0; Ytac0; rewrite (segment_Nat_order1 nN). by rewrite (restriction1_V (proj1 pa) sng qc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)