proposition: Lemma land_ldiff : forall a b, land (ldiff a b) b == 0.
proof: Proof. intros. bitwise. now rewrite <-andb_assoc, (andb_comm (negb _)), andb_negb_r, andb_false_r. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog