proposition: Lemma nbder_pr3 f (g := fun n => (csucc n) *c (f n)): (f \0c = \1c) -> f \1c = \0c -> (forall n, natp n -> f (csucc (csucc n)) = (csucc n) *c (f n +c f (csucc n))) -> (forall n, natp n -> (evenp n) -> f n <> \0c) /\ (forall n, natp n -> f (csucc n) = Yo (evenp n) (cpred (g n)) (csucc (g n))).
proof: Proof. move => pa pb pc. move: succ_zero => s0. have pd': forall n, natp n -> natp (f n) /\ natp (f (csucc n)). apply: Nat_induction; first by rewrite s0 pa pb;split;fprops. move => n nB [hr1 hr2]; split => //; rewrite(pc _ nB); fprops. have pd: (forall n, natp n -> natp (f n)). move => n nN; exact (proj1 (pd' _ nN)). have pe: (forall n, natp n -> f (csucc (csucc n)) <> \0c). apply: Nat_induction. rewrite (pc _ NS0) s0 pa pb (csum0r CS1) (cprod1r CS1); fprops. move => n nN h; move: (NS_succ nN) => h1; rewrite (pc _ h1). move: (cpred_pr (pd _ (NS_succ h1)) h) => [pg ->]. rewrite (csum_nS _ pg);apply: cprod2_nz; apply: succ_nz. have pf: (forall n, natp n -> evenp n -> f n <> \0c). move => n nN en; case: (equal_or_not n \0c). move => ->; rewrite pa; fprops. move => nz; move: (cpred_pr nN nz) => []; set p := (cpred n) => q1 q2. case: (equal_or_not p \0c) => pz. by case: odd_one => [] _; rewrite - succ_zero - pz - q2. move: (cpred_pr q1 pz) => [pp]; rewrite q2 => ->; fprops. split; first by exact. apply: Nat_induction. move: even_zero => h; Ytac0; rewrite /g pa s0 pb -(cpred_pr2 NS0) s0. by rewrite (cprod1r CS1). move => n nN Hrec. have snN:= NS_succ nN. rewrite (pc _ nN) cprodDr. set sn := csucc n. have sa: sn +c \1c = csucc sn by rewrite Nsucc_rw. have ->: Yo (evenp sn) (cpred (g sn)) (csucc (g sn)) = (Yo (evenp sn) (cpred (f sn)) (csucc (f sn))) +c (sn *c f sn). rewrite /g - sa cprodDl csumC (cprod1l (CS_nat (pd _ snN))). Ytac ok; Ytac0; last by rewrite (csum_Sn _ (pd _ snN)) //. case: (equal_or_not (f sn) \0c) => tz. by rewrite tz cprod0r (Nsum0r NS0) cpred0 (Nsum0r NS0). move: (cpred_pr (pd _ snN) tz) => [ta tb]. rewrite {1} tb csum_Sn // cpred_pr1 //; fprops. congr (_ +c (sn *c f sn)). rewrite Hrec /g -/sn. case: (p_or_not_p (evenp n)) => en. move: (proj2 (succ_of_even en)) => nesn; Ytac0; Ytac0. have gnz := (cprod2_nz (@succ_nz n) (pf _ nN en)). by move: (cpred_pr (NS_prod snN (pd _ nN)) gnz)=> [_]. move: (succ_of_odd (conj nN en)) => nesn; Ytac0; Ytac0. rewrite cpred_pr1; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)