Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNo x1.

Assume H2: SNo (mul_SNo x0 x1).

Assume H3: SNo (minus_SNo (mul_SNo x0 x1)).

Assume H4: SNo x2.

Assume H5: SNoLt (mul_SNo x0 x1) x2.

Assume H6: SNo x3.

Assume H7: SNo x4.

Assume H8: SNoLe (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo x2 (mul_SNo x3 x4)).

Assume H9: SNo (mul_SNo x0 x4).

Assume H10: SNo (mul_SNo x3 x4).

Assume H11: SNo (minus_SNo (mul_SNo x3 x4)).

Assume H12: SNo (add_SNo x0 (minus_SNo x3)).

Assume H13: SNo (add_SNo x4 (minus_SNo x1)).

Assume H14: x5 ∈ omega.

Assume H15: SNoLe (eps_ x5) (add_SNo x0 (minus_SNo x3)).

Assume H16: x6 ∈ omega.

Assume H17: SNoLe (eps_ x6) (add_SNo x4 (minus_SNo x1)).

Assume H18: SNo (eps_ x5).

Assume H19: SNo (eps_ x6).

Assume H20: SNo (eps_ (add_SNo x5 x6)).

Assume H21: SNo (mul_SNo (eps_ x5) (eps_ x6)).

Apply SNo_abs_SNo with add_SNo x2 (minus_SNo (mul_SNo x0 x1)).

Apply SNo_add_SNo with x2, minus_SNo (mul_SNo x0 x1) leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H3.

Apply SNoLt_irref with eps_ (add_SNo x5 x6).

Apply SNoLeLt_tra with eps_ (add_SNo x5 x6), abs_SNo (add_SNo x2 (minus_SNo (mul_SNo x0 x1))), eps_ (add_SNo x5 x6) leaving 5 subgoals.

The subproof is completed by applying H20.

The subproof is completed by applying L24.

The subproof is completed by applying H20.

The subproof is completed by applying H23.

The subproof is completed by applying H22.

■

Proofgold Proof