Assume Hs2Q: sqrt2 ∈ rational_numbers.
We will prove False.
We prove the intermediate claim Hirr: sqrt2 ∈ real ∖ rational.
An exact proof term for the current goal is sqrt_2_irrational.
We prove the intermediate claim HnotRat: sqrt2 ∉ rational.
An exact proof term for the current goal is (setminusE2 real rational sqrt2 Hirr).
We prove the intermediate claim HdefQ: rational_numbers = rational.
Use reflexivity.
We prove the intermediate claim Hs2Rat: sqrt2 ∈ rational.
rewrite the current goal using HdefQ (from right to left).
An exact proof term for the current goal is Hs2Q.
An exact proof term for the current goal is (HnotRat Hs2Rat).
∎