proposition: Lemma nbder_pr4 n (g := fun n => (csucc n) *c (nbder n)): natp n -> nbder (csucc n) = Yo (evenp n) (cpred (g n)) (csucc (g n)).
proof: Proof. apply:(proj2 (nbder_pr3 (f:= nbder) nbder_0 nbder_1 nbder_pr2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)