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