proposition: Lemma mul_pred_quot_gt: forall a b, 0<=a -> b<0 -> a < b*(P (a÷b)).
proof: Proof. intros. rewrite <- mul_opp_opp, opp_pred, <- quot_opp_r by order. rewrite <- opp_pos_neg in *. now apply mul_succ_quot_gt. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv