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