proposition: Lemma leB_ltB_trans n (p1 p2 p3: BITS n) : leB p1 p2 -> ltB p2 p3 -> ltB p1 p3.
proof: Proof. move => H1 H2. rewrite leB_nat in H1. rewrite ltB_nat in H2. rewrite ltB_nat. apply: leq_ltn_trans H1 H2. 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)