proposition: Lemma fusc_mean_div2 b (a := cpred b) (c := csucc b): natp b -> b <> \0c -> fusc a +c fusc c = fusc b -> BZcoprime (fuscz a) (fuscz c).
proof: Proof. move => pa pb eq. move:(even_odd_factor pa pb) => [n [p [nN pN eq2]]]. move:(fusc_mean_div nN pN); rewrite - eq2 eq. have fN:=(NS_fusc pa). rewrite -{1} (Nprod1r fN). move /(cprod_eq2l fN NS1 (NS_succ (NS_double nN)) (fusc_nz pa pb)). rewrite - succ_zero => /(csucc_inj CS0 (CS_prod2 _ _)). rewrite - cdouble0 => /(double_inj NS0 nN) => eq3. rewrite /a /c /fuscz eq2 - eq3 cpowx0 (Nprod1l (NS_succ (NS_double pN))). rewrite (cpred_pr1 (CS_prod2 _ _)) (fusc_even pN) - (double_succ pN). rewrite (fusc_even (NS_succ pN)); apply:(fusc_coprime pN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)