proposition: Theorem root_monotonic : forall x y : nat, x * x < y * y -> x < y.
proof: Proof. exact (monotonic_inverse (fun x : nat => x * x) square_monotonic). Qed.
imports: Coq(ArithRing) Coq(Compare_dec) Coq(Wf_nat) Coq(Arith) Coq(Lia)