proposition: Lemma mult_lt_l : forall a b c : nat, 0 < a -> b < c -> a * b < a * c.
proof: Proof. simple induction a. intros; absurd (0 < 0); auto with arith. intros; simpl in |- *. apply lt_le_trans with (c + n * b). rewrite (plus_comm b (n * b)); rewrite (plus_comm c (n * b)); apply plus_lt_compat_l; auto with arith. apply plus_le_compat_l; auto with arith. Qed.
imports: Arith Constants Le_lt_compl