We will prove 2 ∈ R.

We prove the intermediate claim HsumR: add_SNo 1 1 ∈ R.

An exact proof term for the current goal is (real_add_SNo 1 real_1 1 real_1).

rewrite the current goal using add_SNo_1_1_2 (from right to left).

An exact proof term for the current goal is HsumR.

∎