proposition: Lemma andB_mask1: forall n (bs: BITS n), andB bs #1 = (if getBit bs 0 then #1 else #0).
proof: Proof. case=> [bs|n /tupleP [b bs]]. - by rewrite [bs]tuple0 tuple0. - rewrite /andB liftBinOpCons -/andB /= andbT !fromNat0 -/fromNat. rewrite andB0. have ->: getBit [tuple of b :: bs] 0 = b by []. by case: b=> //; rewrite zero_decomp fromNat0. 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