Let x be given.
Assume Hx.
Let g and h be given.
Assume Hgh.
Apply nat_ind to the current goal.
We will prove SNo_sqrtaux x g 0 = SNo_sqrtaux x h 0.
rewrite the current goal using SNo_sqrtaux_0 x g (from left to right).
rewrite the current goal using SNo_sqrtaux_0 x h (from left to right).
We will prove ({g w|w ∈ SNoL_nonneg x},{g z|z ∈ SNoR x}) = ({h w|w ∈ SNoL_nonneg x},{h z|z ∈ SNoR x}).
We prove the intermediate claim L1: {g w|w ∈ SNoL_nonneg x} = {h w|w ∈ SNoL_nonneg x}.
Apply ReplEq_ext (SNoL_nonneg x) g h to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL_nonneg x.
We will prove g w = h w.
Apply SNoL_E x Hx w (SepE1 (SNoL x) (λw ⇒ 0 ≤ w) w Hw) to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
We prove the intermediate claim L2: {g w|w ∈ SNoR x} = {h w|w ∈ SNoR x}.
Apply ReplEq_ext (SNoR x) g h to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
We will prove g w = h w.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
rewrite the current goal using L1 (from left to right).
rewrite the current goal using L2 (from left to right).
Use reflexivity.
Let k be given.
Assume Hk: nat_p k.
Assume IH: SNo_sqrtaux x g k = SNo_sqrtaux x h k.
We will prove SNo_sqrtaux x g (ordsucc k) = SNo_sqrtaux x h (ordsucc k).
rewrite the current goal using SNo_sqrtaux_S x g k Hk (from left to right).
rewrite the current goal using SNo_sqrtaux_S x h k Hk (from left to right).
rewrite the current goal using IH (from left to right).
Use reflexivity.
∎