proposition: Lemma lnot_lor : forall a b, lnot (lor a b) == land (lnot a) (lnot b).
proof: Proof. intros a b. bitwise. now rewrite !lnot_spec, lor_spec, negb_orb. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog