proposition: Lemma lor_neg : forall a b, lor a b < 0 <-> a < 0 \/ b < 0.
proof: Proof. intros a b. rewrite 3 lt_nge, lor_nonneg. split. - apply not_and. apply le_decidable. - now intros [H|H] (H',H''). Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog