proposition: Theorem monotonic_inverse : forall f : nat -> nat, (forall x y : nat, x < y -> f x < f y) -> forall x y : nat, f x < f y -> x < y.
proof: Proof. intros f Hmon x y Hlt; case (le_gt_dec y x); auto. intros Hle; apply Nat.lt_eq_cases in Hle. destruct Hle as [Hlt'|Heq]. elim (Nat.lt_asymm _ _ Hlt); apply Hmon; auto. elim (lt_neq _ _ Hlt); rewrite Heq; auto. Qed.
imports: Coq(ArithRing) Coq(Compare_dec) Coq(Wf_nat) Coq(Arith) Coq(Lia)