proposition: Lemma gcd_n2 n: gcdn n 2 = if (odd n) then 1 else 2.
proof: Proof. by rewrite -{1} (odd_double_half n) -muln2 addnC gcdnC gcdnMDl; case: odd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)