proposition: Lemma lxor_eq_0_iff : forall a a', lxor a a' == 0 <-> a == a'.
proof: Proof. split. - apply lxor_eq. - intros EQ; rewrite EQ; apply lxor_nilpotent. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog