proposition: Theorem Zmult_le_approx n m p : n > 0 -> n > p -> 0 <= m * n + p -> 0 <= m.
proof: Proof. Z.swap_greater. intros. apply Z.lt_succ_r. apply Z.mul_pos_cancel_r with n; trivial. Z.nzsimpl. apply Z.le_lt_trans with (m*n+p); trivial. now apply Z.add_lt_mono_l. Qed.
imports: Arith_base BinInt Zorder Decidable Peano_dec Compare_dec