Let x be given.
Assume Hx.
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7.
Apply real_I to the current goal.
rewrite the current goal using
minus_SNo_invol x Hx1 (from right to left) at position 1.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hx4.
rewrite the current goal using
minus_SNo_invol x Hx1 (from right to left) at position 2.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hx5.
∎