We will prove 3 ∈ R.

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

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

∎