proposition: Lemma addBn_distinct n m : forall (p: BITS n), m.+1 < 2^n -> p <> p +#(m.+1).
proof: Proof. move => p LT. rewrite neqB_modn. rewrite toNat_addB toNat_fromNat. rewrite (@modn_small (m.+1)) => //. rewrite modn_mod. move/eqP. rewrite -{1}(addn0 (toNat p)). rewrite eqn_modDl. rewrite modn_small; last by apply expn_gt0. by rewrite modn_small; last by assumption. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)