proposition: Corollary addBn_ne n m : forall (p: BITS n), m.+1 < 2^n -> p != p +#(m.+1).
proof: Proof. move => p LT. apply/eqP. by apply addBn_distinct. 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)