proposition: Lemma pow2_mod3' n: 2^n = if (odd n) then (3*(((2^n).-2) %/3)).+2 else (3*(((2^n).-1) %/3)).+1.
proof: Proof. rewrite (divn_eq (2^n) 3) pow2_mod3 (mulnC _ 3). by case: odd; rewrite !addnS addn0 /= mulKn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)