proposition: Theorem mul_lt_mono_pos_r : ∀ p n m, 0 < p → p ≠ ∞ → n ≠ ∞ → n < m ↔ n * p < m * p.
proof: Proof. intros p n m Hp Hpi Hni. destruct p as [p| ]; [ simpl | negation Hpi ]. destruct n as [n| ]; [ simpl | negation Hni ]. destruct m as [m| ]; simpl. split; intros. constructor. apply Nat.mul_lt_mono_pos_r; [ inversion Hp | inversion H ]; assumption. constructor. eapply Nat.mul_lt_mono_pos_r; [ inversion Hp | inversion H ]; eassumption. split; intros H; constructor. Qed.
imports: Utf8 Compare_dec NPeano Misc