Apply df_sub__df_neg__df_div__df_nn__df_2__df_3__df_4__df_5__df_6__df_7__df_8__df_9__df_10OLD__df_n0__df_xnn0__df_z__df_dec__df_uz with wceq cz (crab (λ x0 . w3o (wceq (cv x0) cc0) (wcel (cv x0) cn) (wcel (cneg (cv x0)) cn)) (λ x0 . cr)).

Assume H0: wceq cmin (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cc) (λ x0 x1 . crio (λ x2 . wceq (co (cv x1) (cv x2) caddc) (cv x0)) (λ x2 . cc))).

Assume H1: ∀ x0 : ι → ο . wceq (cneg x0) (co cc0 x0 cmin).

Assume H2: wceq cdiv (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cdif cc (csn cc0)) (λ x0 x1 . crio (λ x2 . wceq (co (cv x1) (cv x2) cmul) (cv x0)) (λ x2 . cc))).

Assume H3: wceq cn (cima (crdg (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) c1 caddc)) c1) com).

Assume H4: wceq c2 (co c1 c1 caddc).

Assume H5: wceq c3 (co c2 c1 caddc).

Assume H6: wceq c4 (co c3 c1 caddc).

Assume H7: wceq c5 (co c4 c1 caddc).

Assume H8: wceq c6 (co c5 c1 caddc).

Assume H9: wceq c7 (co c6 c1 caddc).

Assume H10: wceq c8 (co c7 c1 caddc).

Assume H11: wceq c9 (co c8 c1 caddc).

Assume H12: wceq c10 (co c9 c1 caddc).

Assume H13: wceq cn0 (cun cn (csn cc0)).

Assume H14: wceq cxnn0 (cun cn0 (csn cpnf)).

Assume H15: wceq cz (crab (λ x0 . w3o (wceq (cv x0) cc0) (wcel (cv x0) cn) (wcel (cneg (cv x0)) cn)) (λ x0 . cr)).

Assume H16: ∀ x0 x1 : ι → ο . wceq (cdc x0 x1) (co (co (co c9 c1 caddc) x0 cmul) x1 caddc).

Assume H17: wceq cuz (cmpt (λ x0 . cz) (λ x0 . crab (λ x1 . wbr (cv x0) (cv x1) cle) (λ x1 . cz))).

The subproof is completed by applying H15.

■

Proofgold Proof