proposition: Lemma addB0_inv n (p: BITS n) m : m < 2^n -> p == p +# m -> m = 0.
proof: Proof. move => BOUND EQ. destruct n. by destruct m. have: toNat p == toNat (p +# m). by rewrite {1}(eqP EQ). rewrite toNat_addB. rewrite toNat_fromNat. rewrite (@modn_small m); last done. rewrite -{1}(@modn_small (toNat p) (2^n.+1)). rewrite -{1}(addn0 (toNat p)). rewrite eqn_modDl. rewrite modn_small. rewrite modn_small; last done. by move/eqP ->. apply expn_gt0. apply toNatBounded. 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)