We will prove minus_SNo 1 ∈ rational.
We prove the intermediate claim HdefQ: rational_numbers = rational.
Use reflexivity.
We prove the intermediate claim H1rat: 1 ∈ rational.
rewrite the current goal using HdefQ (from right to left) at position 1.
An exact proof term for the current goal is one_in_rational_numbers.
We prove the intermediate claim Hm1rat: minus_SNo 1 ∈ rational.
An exact proof term for the current goal is (rational_minus_SNo 1 H1rat).
rewrite the current goal using HdefQ (from right to left) at position 1.
An exact proof term for the current goal is Hm1rat.
∎