proposition: Lemma leB_nat n (p1 p2: BITS n) : leB p1 p2 = (toNat p1 <= toNat p2).
proof: Proof. rewrite /leB. rewrite ltB_nat. rewrite bitsEq_nat. rewrite orbC. by rewrite (leq_eqVlt (toNat p1)). 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)