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