proposition: Lemma leB_andB: forall n (bs: BITS n) (bs': BITS n), leB (andB bs bs') bs'.
proof: Proof. elim=> [bs bs'|n IHn /tupleP[b bs] /tupleP[b' bs']]. + by rewrite !tuple0 [bs']tuple0. + rewrite /andB liftBinOpCons -/andB /leB /ltB /= !tuple.beheadCons !tuple.theadCons -/ltB. case H: (ltB (andB bs bs') bs'). by rewrite /leB in IHn. have H': (andB bs bs' == bs'). rewrite -[andB _ _ == _]orbF orbC -H. by apply IHn. rewrite H'. move/eqP: H'->. case: b'=> /=. + rewrite !andbT. by case: b=> /=. + by rewrite !andbF orbC orbF //. 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