proposition: Lemma toNat_andB: forall n (bs: BITS n) bs', toNat (andB bs bs') <= toNat bs'.
proof: Proof. elim=> [bs bs'|n IH /tupleP[b bs] /tupleP[b' bs']]. + by rewrite tuple0. + rewrite /andB liftBinOpCons -/andB /=. rewrite /toNat /consB /=. apply leq_add. elim: b=> //. rewrite leq_double. by apply IH. 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