proposition: Theorem mult_lt_reg_l : forall m n p, m * n < m * p -> n < p.
proof: Proof. intros m n; elim n. - intros p; case p. + repeat (rewrite Nat.mul_comm; simpl); auto. + auto with arith. - intros n' Hrec p; case p. + rewrite <- (Nat.mul_comm 0); simpl; intros Hlt; elim (Nat.nlt_0_r (m*S n'));auto. + intros p'; repeat rewrite <- mult_n_Sm. repeat rewrite <- (Nat.add_comm m). intros Hlt; assert (Hlt' : m*n' < m* p'). * apply Nat.add_lt_mono_l with m; auto. * auto with arith. Qed.
imports: List Arith