We will prove 2 ∈ R.

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

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

∎