proposition: Lemma land_nonneg : forall a b, 0 <= land a b <-> 0<=a \/ 0<=b.
proof: Proof. intros a b. now rewrite <- (lnot_involutive (land a b)), lnot_land, lnot_nonneg, lor_neg, !lnot_neg. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog