proposition: Lemma pow2_gt1 n : 1 < 2^n.+1.
proof: Proof. rewrite expnS. suff: 2*1 <= 2*2^n => //. rewrite leq_mul2l/=. apply expn_gt0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div)