proposition: Lemma ltB_nat n : forall p1 p2: BITS n, ltB p1 p2 = (toNat p1 < toNat p2).
proof: Proof. induction n. move => p1 p2. by rewrite (tuple0 p1) (tuple0 p2). move => p1 p2. case/tupleP: p1 => [b1 q1]. case/tupleP: p2 => [b2 q2]. rewrite 2!toNatCons /= !beheadCons !theadCons IHn. case E: (toNat q1 < toNat q2). simpl. case b1; case b2; simpl. + by rewrite ltn_add2l ltn_double. + by rewrite add0n addnC addn1 ltn_Sdouble. + by rewrite add0n addnC addn1 ltnS leq_double ltnW. + by rewrite !add0n ltn_double. case b1; case b2; simpl. + rewrite ltn_add2l ltn_double E. by rewrite andbF. + rewrite add0n addnC addn1 ltn_Sdouble E. by rewrite andbF. + rewrite add0n addnC addn1 ltnS leq_double. rewrite !andbT. rewrite leq_eqVlt E. rewrite orbF. apply bitsEq_nat. + rewrite !add0n ltn_double E. by rewrite andbF. 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)