proposition: Theorem le_mult : forall m n p q : nat, n <= p -> m <= q -> n * m <= p * q.
proof: Proof. intros m n p q H1 H2; apply Nat.le_trans with (p * m); auto with arith. repeat rewrite (fun x => Nat.mul_comm x m); auto with arith. Qed.
imports: Coq(Arith ArithRing)