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.