proposition: Theorem square_monotonic : forall x y : nat, x < y -> x * x < y * y.
proof: Proof. intros x; case x. intros y; case y; simpl in |- *; auto with *. intros x' y Hlt; apply Nat.lt_trans with (S x' * y). rewrite (Nat.mul_comm (S x') y); apply mult_lt; auto. apply mult_lt; lia. Qed.
imports: Coq(ArithRing) Coq(Compare_dec) Coq(Wf_nat) Coq(Arith) Coq(Lia)