Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Assume H0: nat_p x2.

Let x3 of type ι be given.

Assume H1: nat_p x3.

Assume H2: x2 ⊆ x3.

Apply nat_Subq_add_ex with x2, x3, and (ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 x3) 0) (ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 x3) 1) leaving 4 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Let x4 of type ι be given.

Assume H3: (λ x5 . and (nat_p x5) (x3 = add_nat x5 x2)) x4.

Apply H3 with and (ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 x3) 0) (ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 x3) 1).

Assume H4: nat_p x4.

Apply add_nat_com with x4, x2, λ x5 x6 . x3 = x6 ⟶ and (ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 x3) 0) (ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 x3) 1) leaving 3 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H0.

Assume H5: x3 = add_nat x2 x4.

Apply H5 with λ x5 x6 . and (ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 x6) 0) (ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 x6) 1).

Apply SNo_sqrtaux_mon_lem with x0, x1, x2, x4 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H4.

■

Proofgold Proof