proposition: Lemma le_mult_l : forall p q : nat, p <= q -> forall r : nat, r * p <= r * q.
proof: Proof. intros p q H. simple induction r. simpl in |- *. apply le_n. intros r1 IHr1. simpl in |- *. apply plus_le_compat. assumption. assumption. Qed.
imports: ZArith EqNat