We prove the intermediate claim L_add_4_inner_mid: ∀x y z w, F x → F y → F z → F w → (x + y) + (z + w) = (x + z) + (y + w).

Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

rewrite the current goal using F_add_assoc (x + y) z w (F_add x y Hx Hy) Hz Hw (from right to left).

We will prove ((x + y) + z) + w = (x + z) + (y + w).

rewrite the current goal using F_add_assoc x y z Hx Hy Hz (from left to right).

We will prove (x + (y + z)) + w = (x + z) + (y + w).

rewrite the current goal using F_add_com y z Hy Hz (from left to right).

We will prove (x + (z + y)) + w = (x + z) + (y + w).

rewrite the current goal using F_add_assoc x z y Hx Hz Hy (from right to left).

We will prove ((x + z) + y) + w = (x + z) + (y + w).

An exact proof term for the current goal is F_add_assoc (x + z) y w (F_add x z Hx Hz) Hy Hw.

Let z, w and u be given.

Assume Hz Hw Hu.

We prove the intermediate claim Lp0z: F (proj0 z).

An exact proof term for the current goal is CD_proj0R z Hz.

We prove the intermediate claim Lp1z: F (proj1 z).

An exact proof term for the current goal is CD_proj1R z Hz.

We prove the intermediate claim Lp0w: F (proj0 w).

An exact proof term for the current goal is CD_proj0R w Hw.

We prove the intermediate claim Lp1w: F (proj1 w).

An exact proof term for the current goal is CD_proj1R w Hw.

We prove the intermediate claim Lp0u: F (proj0 u).

An exact proof term for the current goal is CD_proj0R u Hu.

We prove the intermediate claim Lp1u: F (proj1 u).

An exact proof term for the current goal is CD_proj1R u Hu.

We prove the intermediate claim Lp0zw: F (proj0 z + proj0 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zw: F (proj1 z + proj1 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp0u: F (conj (proj0 u)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1u: F (conj (proj1 u)).

Apply F_conj to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp0zp0u: F (proj0 z * proj0 u).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1up1z: F (conj (proj1 u) * proj1 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1up1z: F (- conj (proj1 u) * proj1 z).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzuL: F (proj0 z * proj0 u + - conj (proj1 u) * proj1 z).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1up0z: F (proj1 u * proj0 z).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1zcp0u: F (proj1 z * conj (proj0 u)).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LzuR: F (proj1 u * proj0 z + proj1 z * conj (proj0 u)).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp0wp0u: F (proj0 w * proj0 u).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1up1w: F (conj (proj1 u) * proj1 w).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lcp1up1w: F (- conj (proj1 u) * proj1 w).

Apply F_minus to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LwuL: F (proj0 w * proj0 u + - conj (proj1 u) * proj1 w).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1up0w: F (proj1 u * proj0 w).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim Lp1wcp0u: F (proj1 w * conj (proj0 u)).

Apply F_mul to the current goal.

An exact proof term for the current goal is ??.

We prove the intermediate claim LwuR: F (proj1 u * proj0 w + proj1 w * conj (proj0 u)).

Apply F_add to the current goal.

An exact proof term for the current goal is ??.

Set zw to be the term pa (proj0 z + proj0 w) (proj1 z + proj1 w).

Set zu to be the term pa (proj0 z * proj0 u + - conj (proj1 u) * proj1 z) (proj1 u * proj0 z + proj1 z * conj (proj0 u)).

Set wu to be the term pa (proj0 w * proj0 u + - conj (proj1 u) * proj1 w) (proj1 u * proj0 w + proj1 w * conj (proj0 u)).

We will prove pa (proj0 zw * proj0 u + - conj (proj1 u) * proj1 zw) (proj1 u * proj0 zw + proj1 zw * conj (proj0 u)) = pa (proj0 zu + proj0 wu) (proj1 zu + proj1 wu).

rewrite the current goal using CD_proj0_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 z + proj0 w) (proj1 z + proj1 w) ?? ?? (from left to right).

We will prove pa ((proj0 z + proj0 w) * proj0 u + - conj (proj1 u) * (proj1 z + proj1 w)) (proj1 u * (proj0 z + proj0 w) + (proj1 z + proj1 w) * conj (proj0 u)) = pa (proj0 zu + proj0 wu) (proj1 zu + proj1 wu).

rewrite the current goal using CD_proj0_2 (proj0 z * proj0 u + - conj (proj1 u) * proj1 z) (proj1 u * proj0 z + proj1 z * conj (proj0 u)) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 z * proj0 u + - conj (proj1 u) * proj1 z) (proj1 u * proj0 z + proj1 z * conj (proj0 u)) ?? ?? (from left to right).

rewrite the current goal using CD_proj0_2 (proj0 w * proj0 u + - conj (proj1 u) * proj1 w) (proj1 u * proj0 w + proj1 w * conj (proj0 u)) ?? ?? (from left to right).

rewrite the current goal using CD_proj1_2 (proj0 w * proj0 u + - conj (proj1 u) * proj1 w) (proj1 u * proj0 w + proj1 w * conj (proj0 u)) ?? ?? (from left to right).

Use f_equal.

We will prove (proj0 z + proj0 w) * proj0 u + - conj (proj1 u) * (proj1 z + proj1 w) = (proj0 z * proj0 u + - conj (proj1 u) * proj1 z) + (proj0 w * proj0 u + - conj (proj1 u) * proj1 w).

rewrite the current goal using L_add_4_inner_mid (proj0 z * proj0 u) (- conj (proj1 u) * proj1 z) (proj0 w * proj0 u) (- conj (proj1 u) * proj1 w) ?? ?? ?? ?? (from left to right).

Use f_equal.

We will prove (proj0 z + proj0 w) * proj0 u = proj0 z * proj0 u + proj0 w * proj0 u.

Apply F_add_mul_distrR to the current goal.

An exact proof term for the current goal is ??.

We will prove - conj (proj1 u) * (proj1 z + proj1 w) = (- conj (proj1 u) * proj1 z) + (- conj (proj1 u) * proj1 w).

rewrite the current goal using F_minus_add (conj (proj1 u) * proj1 z) (conj (proj1 u) * proj1 w) ?? ?? (from right to left).

Use f_equal.

We will prove conj (proj1 u) * (proj1 z + proj1 w) = (conj (proj1 u) * proj1 z) + (conj (proj1 u) * proj1 w).

Apply F_add_mul_distrL to the current goal.

An exact proof term for the current goal is ??.

We will prove (proj1 u * (proj0 z + proj0 w) + (proj1 z + proj1 w) * conj (proj0 u)) = (proj1 u * proj0 z + proj1 z * conj (proj0 u)) + (proj1 u * proj0 w + proj1 w * conj (proj0 u)).

rewrite the current goal using L_add_4_inner_mid (proj1 u * proj0 z) (proj1 z * conj (proj0 u)) (proj1 u * proj0 w) (proj1 w * conj (proj0 u)) ?? ?? ?? ?? (from left to right).

Use f_equal.

Apply F_add_mul_distrL to the current goal.

An exact proof term for the current goal is ??.

Apply F_add_mul_distrR to the current goal.

An exact proof term for the current goal is ??.

∎