proposition: Lemma leB_weaken n (p1 p2: BITS n) : ltB p1 p2 -> leB p1 p2.
proof: Proof. move => H. by rewrite /leB H. 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)