proposition: Lemma pow2_mod3 n: 2^n %% 3 = 1 + odd n.
proof: Proof. by elim:n => // n Hr /=; rewrite expnS -modnMm Hr; case: odd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)