proposition: Lemma pow2_sub_ltn n x : (2^n)-(x.+1) < 2^n.
proof: Proof. have H := expn_gt0 2 n. simpl in H. destruct (nat_lt0_succ H) as [m' HH]. rewrite HH. rewrite addn1 subSS. by rewrite ltnS leq_subr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div)