proposition: Theorem mul_lt_mono_nonneg : forall n m p q, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
proof: Proof. intros n m p q H1 H2 H3 H4. apply le_lt_trans with (m * p). - apply mul_le_mono_nonneg_r; [assumption | now apply lt_le_incl]. - apply -> mul_lt_mono_pos_l; [assumption | now apply le_lt_trans with n]. Qed.
imports: NZAxioms NZAddOrder