How to prove f x < f y → x ≢ y

Question

module badequality where
open import Relation.Binary.PropositionalEquality
open import Data.Nat using (ℕ; zero; suc; _<_)
open import Data.Empty using (⊥; ⊥-elim)

postulate
  f : ℕ → ℕ

anti-cong : {x y : ℕ} → f x < f y → x ≢ y
anti-cong fx<fy = {!   !} 

How to prove above anti-cong, or it only can be introduced by postulate.

Answer 1

Sure: you can use the fact that _<_ is irreflexive to derive a contradiction from the assumption that both f x < f y and x ≡ y are true.

This is how it goes:

open import Data.Nat.Properties using (<-irrefl)

anti-cong : {x y : ℕ} → f x < f y → x ≢ y
anti-cong fx<fy x≡y = <-irrefl (cong f x≡y) fx<fy

Answer 2

Motivated by @gallais's solution, I think there is a more natural solution:

We can prove contraposition first, which is (A → B) → (¬ B → ¬ A). Then we prove x ≡ y → f x ≥ f y, which is the contrapositive of original proposition. Finally, we apply contraposition to the contrapositive. Here is my code

open import Data.Nat using (ℕ; zero; suc; _<_; _≥_)
open import Data.Nat.Properties using (≤-reflexive; <⇒≱)
open import Relation.Nullary using (¬_)

contraposition : ∀ {A B : Set} → (A → B) → (¬ B → ¬ A)
contraposition f ¬b a = ¬b (f a)

=≥ : {x y : ℕ} → x ≡ y → f x ≥ f y
=≥ x=y = ≤-reflexive (cong f (sym x=y))  

anti-cong : {x y : ℕ} → f x < f y → x ≢ y
anti-cong {x} {y} fx<fy = contraposition (=≥ {x} {y}) (<⇒≱ fx<fy)