proposition: Lemma lnot_lxor_r : forall a b, lnot (lxor a b) == lxor a (lnot b).
proof: Proof. intros a b. bitwise. now rewrite !lnot_spec, !lxor_spec, negb_xorb_r. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog