proposition: Theorem le_mult_right : forall x y : nat, 0 < y -> x <= x * y.
proof: Proof. intros x y; case y. intros H'; Contradict H'; auto with arith. intros n H'; rewrite Nat.mul_comm; simpl in |- *; auto with arith. Qed.
imports: Coq(Arith ArithRing)