proposition: Lemma fusc_mean_div1 b (a := cpred b) (c := csucc b): natp b -> b <> \0c -> exists2 n, natp n &fusc a +c fusc c = (fusc b) *c csucc (cdouble n).
proof: Proof. move => pa pb. move:(even_odd_factor pa pb) => [n [p [nN pN eq]]]. by move:(fusc_mean_div nN pN); rewrite - eq => h; exists n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)