proposition: Lemma lor_ldiff_and : forall a b, lor (ldiff a b) (land a b) == a.
proof: Proof. intros. bitwise. now rewrite <- andb_orb_distrib_r, orb_comm, orb_negb_r, andb_true_r. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog