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