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