proposition: Lemma orB_invB: forall n (bs: BITS n), orB bs (invB bs) = ones n.
proof: Proof. move=> n bs. apply allBitsEq=> k le_k. rewrite getBit_liftBinOp =>//. rewrite getBit_liftUnOp =>//. by rewrite orbN /getBit nth_nseq le_k. 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