proposition: Lemma toNat_subB n (p q: BITS n) : leB q p -> toNat (subB p q) = toNat p - toNat q.
proof: Proof. move => LE. have P := toNatBounded p. have Q := toNatBounded q. case E: (p == q). rewrite (eqP E). by rewrite subBB toNat_fromNat0 subnn. rewrite subB_equiv_addB_negB. rewrite toNat_addB. rewrite toNat_negB. case E': (toNat q == 0). rewrite (eqP E') subn0 addn0. rewrite modn_small //. rewrite addnBA; last first. apply ltnW => //. rewrite addnC. rewrite -addnBA. rewrite modnDl. rewrite modn_small => //. have H : (toNat p - toNat q <= toNat p) by apply leq_subr. apply: leq_ltn_trans H P. by rewrite leB_nat in LE. 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)