proposition: Lemma odd_power2subn1 n : odd ((2^(n.+1)).-1) = true.
proof: Proof. induction n => //. rewrite expnS mul2n odd_oddsubn1. by rewrite odd_double. rewrite -mul2n -expnS. apply expn_gt0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div)