proposition: Lemma mul_pred_quot_lt: forall a b, a<=0 -> 0<b -> b*(P (a÷b)) < a.
proof: Proof. intros. rewrite opp_lt_mono, <- mul_opp_r, opp_pred, <- quot_opp_l by order. rewrite <- opp_nonneg_nonpos in *. now apply mul_succ_quot_gt. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv