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