proposition: Lemma subB_addB n (p: BITS n) m1 m2 : p -# m1 +# m2 = if m1<m2 then p +# (m2-m1) else p -# (m1-m2).
proof: Proof. destruct n; first apply trivialBits. case E: (m1 < m2). apply toZp_inj. autorewrite with ZpHom. rewrite natrB. rewrite addrAC. by rewrite addrA. by apply ltnW. apply toZp_inj. autorewrite with ZpHom. rewrite natrB. rewrite addrAC. rewrite opprB. by rewrite addrA. rewrite leqNgt. by rewrite E. 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)