proposition: Lemma addBsubBn n (p: BITS n) m1 m2 : m2 <= m1 -> p +# (m1-m2) = p +# m1 -# m2.
proof: Proof. move => H. destruct n; first apply trivialBits. apply toZp_inj. autorewrite with ZpHom. rewrite natrB => //. by rewrite addrA. 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)