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