proposition: Lemma lxor_eq : forall a a', lxor a a' == 0 -> a == a'.
proof: Proof. intros a a' H. bitwise. apply xorb_eq. now rewrite <- lxor_spec, H, bits_0. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog