proposition: Lemma lt_mult_l : forall p q : nat, p < q -> forall r : nat, S r * p < S r * q.
proof: Proof. intros p q H. simple induction r. simpl in |- *. rewrite <- plus_n_O. rewrite <- plus_n_O. assumption. intros r1 IHr1. simpl in |- *. apply lt_plus_plus. assumption. assumption. Qed.
imports: ZArith EqNat