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 Lp0wu: F (proj0 w + proj0 u).

Apply F_add to the current goal.

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

We prove the intermediate claim Lp1wu: F (proj1 w + proj1 u).

Apply F_add to the current goal.

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

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

Apply F_conj to the current goal.

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

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

Apply F_conj 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 Lp0zp0w: F (proj0 z * proj0 w).

Apply F_mul to the current goal.

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

We prove the intermediate claim Lcp1wp1z: F (conj (proj1 w) * proj1 z).

Apply F_mul to the current goal.

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

We prove the intermediate claim Lcp1wp1z: F (- conj (proj1 w) * proj1 z).

Apply F_minus to the current goal.

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

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

Apply F_add to the current goal.

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

We prove the intermediate claim Lp1wp0z: F (proj1 w * proj0 z).

Apply F_mul to the current goal.

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

We prove the intermediate claim Lp1zcp0w: F (proj1 z * conj (proj0 w)).

Apply F_mul to the current goal.

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

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

Apply F_add 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 ??.

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

Set zw to be the term pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 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)).

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

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

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

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

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

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).

Use f_equal.

rewrite the current goal using L_add_4_inner_mid (proj0 z * proj0 w) (- conj (proj1 w) * proj1 z) (proj0 z * proj0 u) (- conj (proj1 u) * proj1 z) ?? ?? ?? ?? (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 ??.

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

rewrite the current goal using F_conj_add (proj1 w) (proj1 u) ?? ?? (from left to right).

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

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

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

Apply F_minus_add to the current goal.

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

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

Use f_equal.

Apply F_add_mul_distrR to the current goal.

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

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

rewrite the current goal using F_conj_add (proj0 w) (proj0 u) ?? ?? (from left to right).

Apply F_add_mul_distrL to the current goal.

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

∎