proposition: Lemma neqB_modn n (p q: BITS n) : p <> q <-> toNat p <> toNat q %[mod 2^n].
proof: Proof. split => H. move => H'. rewrite (@modn_small (toNat p)) in H'. rewrite (@modn_small (toNat q)) in H'. apply toNat_inj in H'. by subst. apply toNatBounded. apply toNatBounded. move => H'. by subst. 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)