proposition: Lemma andB_invB: forall n (bs: BITS n), andB bs (invB bs) = zero n.
proof: Proof. move=> n bs. apply allBitsEq. move=> k le_k. rewrite getBit_liftBinOp =>//. rewrite getBit_liftUnOp =>//. by rewrite andbN -fromNat0 getBit_zero. 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