Beginning of Section SurQuaternions
Theorem. (quaternion_tag_fresh)
∀z, CSNo z → ∀u ∈ z, {3} ∉ u
In Proofgold the corresponding term root is 202f04... and proposition id is cbed07...
Proof:
Let z be given.
Assume Hz.
Apply Sing_nat_fresh_extension 3 nat_3 In_1_3 z to the current goal.
We will prove ExtendedSNoElt_ 3 z.
An exact proof term for the current goal is CSNo_ExtendedSNoElt_3 z Hz.
∎
Definition. We define CSNo_pair to be pair_tag {3} of type set → set → set.
In Proofgold the corresponding term root is 6ad954... and object id is bd2d99...
Theorem. (CSNo_pair_0)
∀x, CSNo_pair x 0 = x
In Proofgold the corresponding term root is 4db8eb... and proposition id is abfae9...
Proof:
An exact proof term for the current goal is pair_tag_0 {3} CSNo quaternion_tag_fresh.
∎
Theorem. (CSNo_pair_prop_1)
∀x1 y1 x2 y2, CSNo x1 → CSNo x2 → CSNo_pair x1 y1 = CSNo_pair x2 y2 → x1 = x2
In Proofgold the corresponding term root is 232223... and proposition id is b34370...
Proof:
An exact proof term for the current goal is pair_tag_prop_1 {3} CSNo quaternion_tag_fresh.
∎
Theorem. (CSNo_pair_prop_2)
∀x1 y1 x2 y2, CSNo x1 → CSNo y1 → CSNo x2 → CSNo y2 → CSNo_pair x1 y1 = CSNo_pair x2 y2 → y1 = y2
In Proofgold the corresponding term root is 225c4f... and proposition id is 9ff93a...
Proof:
An exact proof term for the current goal is pair_tag_prop_2 {3} CSNo quaternion_tag_fresh.
∎
Definition. We define HSNo to be CD_carr {3} CSNo of type set → prop.
In Proofgold the corresponding term root is 1e7352... and object id is 89bf4d...
Theorem. (HSNo_I)
∀x y, CSNo x → CSNo y → HSNo (CSNo_pair x y)
In Proofgold the corresponding term root is 17ad60... and proposition id is 8476c5...
Proof:
An exact proof term for the current goal is CD_carr_I {3} CSNo quaternion_tag_fresh.
∎
Theorem. (HSNo_E)
∀z, HSNo z → ∀p : set → prop, (∀x y, CSNo x → CSNo y → z = CSNo_pair x y → p (CSNo_pair x y)) → p z
In Proofgold the corresponding term root is 318e94... and proposition id is a9207a...
Proof:
An exact proof term for the current goal is CD_carr_E {3} CSNo quaternion_tag_fresh.
∎
Theorem. (CSNo_HSNo)
∀x, CSNo x → HSNo x
In Proofgold the corresponding term root is 307398... and proposition id is 0db147...
Proof:
An exact proof term for the current goal is CD_carr_0ext {3} CSNo quaternion_tag_fresh CSNo_0.
∎
Theorem. (HSNo_0)
HSNo 0
In Proofgold the corresponding term root is 27cacb... and proposition id is d3c9ac...
Proof:
Apply CSNo_HSNo to the current goal.
An exact proof term for the current goal is CSNo_0.
∎
Theorem. (HSNo_1)
HSNo 1
In Proofgold the corresponding term root is 3065de... and proposition id is ca7c07...
Proof:
Apply CSNo_HSNo to the current goal.
An exact proof term for the current goal is CSNo_1.
∎
Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha {3}
Notation. We use '' as a postfix operator with priority 100 corresponding to applying term ctag.
Theorem. (HSNo_ExtendedSNoElt_4)
∀z, HSNo z → ExtendedSNoElt_ 4 z
In Proofgold the corresponding term root is 4407d8... and proposition id is d88675...
Proof:
Let z be given.
Assume Hz.
Apply HSNo_E z Hz to the current goal.
Let x and y be given.
Assume Hx: CSNo x.
Assume Hy: CSNo y.
Assume Hzxy: z = CSNo_pair x y.
Let v be given.
Assume Hv: v ∈ ⋃ (CSNo_pair x y).
Apply UnionE_impred (CSNo_pair x y) v Hv to the current goal.
Let u be given.
Assume H1: v ∈ u.
Assume H2: u ∈ CSNo_pair x y.
Apply binunionE x {w ''|w ∈ y} u H2 to the current goal.
Assume H3: u ∈ x.
We prove the intermediate claim L1: v ∈ ⋃ x.
An exact proof term for the current goal is UnionI x v u H1 H3.
We will prove ordinal v ∨ ∃i ∈ 4, v = {i}.
An exact proof term for the current goal is extension_SNoElt_mon 3 4 (ordsuccI1 3) x (CSNo_ExtendedSNoElt_3 x Hx) v L1.
Assume H3: u ∈ {w ''|w ∈ y}.
Apply ReplE_impred y ctag u H3 to the current goal.
Let w be given.
Assume Hw: w ∈ y.
Assume H4: u = w ''.
We prove the intermediate claim L2: v ∈ w ''.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H1.
Apply binunionE w {{3}} v L2 to the current goal.
Assume H5: v ∈ w.
We prove the intermediate claim L3: v ∈ ⋃ y.
An exact proof term for the current goal is UnionI y v w H5 Hw.
An exact proof term for the current goal is extension_SNoElt_mon 3 4 (ordsuccI1 3) y (CSNo_ExtendedSNoElt_3 y Hy) v L3.
Assume H5: v ∈ {{3}}.
We will prove ordinal v ∨ ∃i ∈ 4, v = {i}.
Apply orIR to the current goal.
We use 3 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 3 ∈ 4.
An exact proof term for the current goal is In_3_4.
We will prove v = {3}.
An exact proof term for the current goal is SingE {3} v H5.
∎
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_CSNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_CSNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_CSNo.
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_CSNo.
Notation. We use ' as a postfix operator with priority 100 corresponding to applying term conj_CSNo.
Let i ≝ Complex_i
Definition. We define Quaternion_j to be CSNo_pair 0 1 of type set.
In Proofgold the corresponding term root is c0b7d8... and object id is 834439...
Definition. We define Quaternion_k to be CSNo_pair 0 i of type set.
In Proofgold the corresponding term root is 7dfb3a... and object id is 3ae5b3...
Let j ≝ Quaternion_j
Let k ≝ Quaternion_k
Definition. We define HSNo_proj0 to be CD_proj0 {3} CSNo of type set → set.
In Proofgold the corresponding term root is 93f0b6... and object id is 0380b7...
Definition. We define HSNo_proj1 to be CD_proj1 {3} CSNo of type set → set.
In Proofgold the corresponding term root is bc3d4d... and object id is c8e617...
Let p0 : set → set ≝ HSNo_proj0
Let p1 : set → set ≝ HSNo_proj1
Let pa : set → set → set ≝ CSNo_pair
Theorem. (HSNo_proj0_1)
∀z, HSNo z → CSNo (p0 z) ∧ ∃y, CSNo y ∧ z = pa (p0 z) y
In Proofgold the corresponding term root is 47baad... and proposition id is d8e2ef...
Proof:
An exact proof term for the current goal is CD_proj0_1 {3} CSNo quaternion_tag_fresh.
∎
Theorem. (HSNo_proj0_2)
∀x y, CSNo x → CSNo y → p0 (pa x y) = x
In Proofgold the corresponding term root is 9ffb4a... and proposition id is 57a042...
Proof:
An exact proof term for the current goal is CD_proj0_2 {3} CSNo quaternion_tag_fresh.
∎
Theorem. (HSNo_proj1_1)
∀z, HSNo z → CSNo (p1 z) ∧ z = pa (p0 z) (p1 z)
In Proofgold the corresponding term root is d65060... and proposition id is b38fa3...
Proof:
An exact proof term for the current goal is CD_proj1_1 {3} CSNo quaternion_tag_fresh.
∎
Theorem. (HSNo_proj1_2)
∀x y, CSNo x → CSNo y → p1 (pa x y) = y
In Proofgold the corresponding term root is 2c4d65... and proposition id is b8596e...
Proof:
An exact proof term for the current goal is CD_proj1_2 {3} CSNo quaternion_tag_fresh.
∎
Theorem. (HSNo_proj0R)
∀z, HSNo z → CSNo (p0 z)
In Proofgold the corresponding term root is dfba9c... and proposition id is d5b6be...
Proof:
An exact proof term for the current goal is CD_proj0R {3} CSNo quaternion_tag_fresh.
∎
Theorem. (HSNo_proj1R)
∀z, HSNo z → CSNo (p1 z)
In Proofgold the corresponding term root is 88c956... and proposition id is 4c5b7f...
Proof:
An exact proof term for the current goal is CD_proj1R {3} CSNo quaternion_tag_fresh.
∎
Theorem. (HSNo_proj0p1)
∀z, HSNo z → z = pa (p0 z) (p1 z)
In Proofgold the corresponding term root is 099ef1... and proposition id is cd06de...
Proof:
An exact proof term for the current goal is CD_proj0proj1_eta {3} CSNo quaternion_tag_fresh.
∎
Theorem. (HSNo_proj0proj1_split)
∀z w, HSNo z → HSNo w → p0 z = p0 w → p1 z = p1 w → z = w
In Proofgold the corresponding term root is 878bb6... and proposition id is 4cfedf...
Proof:
An exact proof term for the current goal is CD_proj0proj1_split {3} CSNo quaternion_tag_fresh.
∎
Definition. We define HSNoLev to be λz ⇒ CSNoLev (p0 z) ∪ CSNoLev (p1 z) of type set → set.
In Proofgold the corresponding term root is 7ed157... and object id is c05a12...
Theorem. (HSNoLev_ordinal)
∀z, HSNo z → ordinal (HSNoLev z)
In Proofgold the corresponding term root is 5fdf84... and proposition id is c12b44...
Proof:
Let z be given.
Assume Hz.
Apply HSNo_E z Hz to the current goal.
Let x and y be given.
Assume Hx Hy.
Assume Hzxy: z = pa x y.
We will prove ordinal (CSNoLev (p0 (pa x y)) ∪ CSNoLev (p1 (pa x y))).
rewrite the current goal using HSNo_proj0_2 x y Hx Hy (from left to right).
rewrite the current goal using HSNo_proj1_2 x y Hx Hy (from left to right).
We will prove ordinal (CSNoLev x ∪ CSNoLev y).
An exact proof term for the current goal is ordinal_binunion (CSNoLev x) (CSNoLev y) (CSNoLev_ordinal x Hx) (CSNoLev_ordinal y Hy).
∎
Definition. We define minus_HSNo to be CD_minus {3} CSNo minus_CSNo of type set → set.
In Proofgold the corresponding term root is f59664... and object id is b481a7...
Definition. We define conj_HSNo to be CD_conj {3} CSNo minus_CSNo conj_CSNo of type set → set.
In Proofgold the corresponding term root is 87fd0c... and object id is 66366c...
Definition. We define add_HSNo to be CD_add {3} CSNo add_CSNo of type set → set → set.
In Proofgold the corresponding term root is a3bb10... and object id is 3681e1...
Definition. We define mul_HSNo to be CD_mul {3} CSNo minus_CSNo conj_CSNo add_CSNo mul_CSNo of type set → set → set.
In Proofgold the corresponding term root is e7bde6... and object id is 34cbed...
Definition. We define exp_HSNo_nat to be CD_exp_nat {3} CSNo minus_CSNo conj_CSNo add_CSNo mul_CSNo of type set → set → set.
In Proofgold the corresponding term root is b3bc74... and object id is 121913...
Let plus' ≝ add_HSNo
Let mult' ≝ mul_HSNo
Notation. We use :-: as a prefix operator with priority 358 corresponding to applying term minus_HSNo.
Notation. We use '' as a postfix operator with priority 100 corresponding to applying term conj_HSNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_HSNo.
Notation. We use ⨯ as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_HSNo.
Notation. We use :^: as an infix operator with priority 355 and which associates to the right corresponding to applying term exp_HSNo_nat.
Theorem. (HSNo_Complex_i)
HSNo i
In Proofgold the corresponding term root is 1c2523... and proposition id is 9eee28...
Proof:
Apply CSNo_HSNo to the current goal.
An exact proof term for the current goal is CSNo_Complex_i.
∎
Theorem. (HSNo_Quaternion_j)
HSNo j
In Proofgold the corresponding term root is 498a34... and proposition id is 4e668f...
Proof:
We will prove HSNo (pa 0 1).
Apply HSNo_I to the current goal.
An exact proof term for the current goal is CSNo_0.
An exact proof term for the current goal is CSNo_1.
∎
Theorem. (HSNo_Quaternion_k)
HSNo k
In Proofgold the corresponding term root is 5a2d44... and proposition id is 7b6e43...
Proof:
We will prove HSNo (pa 0 i).
Apply HSNo_I to the current goal.
An exact proof term for the current goal is CSNo_0.
An exact proof term for the current goal is CSNo_Complex_i.
∎
Theorem. (HSNo_minus_HSNo)
∀z, HSNo z → HSNo (minus_HSNo z)
In Proofgold the corresponding term root is e82f65... and proposition id is f8d185...
Proof:
An exact proof term for the current goal is CD_minus_CD {3} CSNo quaternion_tag_fresh minus_CSNo CSNo_minus_CSNo.
∎
Theorem. (minus_HSNo_proj0)
∀z, HSNo z → p0 (:-: z) = - p0 z
In Proofgold the corresponding term root is 0f68d7... and proposition id is b166fc...
Proof:
An exact proof term for the current goal is CD_minus_proj0 {3} CSNo quaternion_tag_fresh minus_CSNo CSNo_minus_CSNo.
∎
Theorem. (minus_HSNo_proj1)
∀z, HSNo z → p1 (:-: z) = - p1 z
In Proofgold the corresponding term root is 26353b... and proposition id is bd1384...
Proof:
An exact proof term for the current goal is CD_minus_proj1 {3} CSNo quaternion_tag_fresh minus_CSNo CSNo_minus_CSNo.
∎
Theorem. (HSNo_conj_HSNo)
∀z, HSNo z → HSNo (conj_HSNo z)
In Proofgold the corresponding term root is 2747f5... and proposition id is 67a2db...
Proof:
An exact proof term for the current goal is CD_conj_CD {3} CSNo quaternion_tag_fresh minus_CSNo CSNo_minus_CSNo conj_CSNo CSNo_conj_CSNo.
∎
Theorem. (conj_HSNo_proj0)
∀z, HSNo z → p0 (z '') = (p0 z) '
In Proofgold the corresponding term root is c3731a... and proposition id is b3ff6d...
Proof:
An exact proof term for the current goal is CD_conj_proj0 {3} CSNo quaternion_tag_fresh minus_CSNo CSNo_minus_CSNo conj_CSNo CSNo_conj_CSNo.
∎
Theorem. (conj_HSNo_proj1)
∀z, HSNo z → p1 (z '') = - p1 z
In Proofgold the corresponding term root is 07def3... and proposition id is 686476...
Proof:
An exact proof term for the current goal is CD_conj_proj1 {3} CSNo quaternion_tag_fresh minus_CSNo CSNo_minus_CSNo conj_CSNo CSNo_conj_CSNo.
∎
Theorem. (HSNo_add_HSNo)
∀z w, HSNo z → HSNo w → HSNo (add_HSNo z w)
In Proofgold the corresponding term root is 37bb2a... and proposition id is 1f7aba...
Proof:
An exact proof term for the current goal is CD_add_CD {3} CSNo quaternion_tag_fresh add_CSNo CSNo_add_CSNo.
∎
Theorem. (add_HSNo_proj0)
∀z w, HSNo z → HSNo w → p0 (plus' z w) = p0 z + p0 w
In Proofgold the corresponding term root is 3f6ec4... and proposition id is 565511...
Proof:
An exact proof term for the current goal is CD_add_proj0 {3} CSNo quaternion_tag_fresh add_CSNo CSNo_add_CSNo.
∎
Theorem. (add_HSNo_proj1)
∀z w, HSNo z → HSNo w → p1 (plus' z w) = p1 z + p1 w
In Proofgold the corresponding term root is 5b2438... and proposition id is 9fce86...
Proof:
An exact proof term for the current goal is CD_add_proj1 {3} CSNo quaternion_tag_fresh add_CSNo CSNo_add_CSNo.
∎
Theorem. (HSNo_mul_HSNo)
∀z w, HSNo z → HSNo w → HSNo (z ⨯ w)
In Proofgold the corresponding term root is 25d347... and proposition id is 5382cd...
Proof:
An exact proof term for the current goal is CD_mul_CD {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_minus_CSNo CSNo_conj_CSNo CSNo_add_CSNo CSNo_mul_CSNo.
∎
Theorem. (mul_HSNo_proj0)
∀z w, HSNo z → HSNo w → p0 (mult' z w) = p0 z * p0 w + - (p1 w ' * p1 z)
In Proofgold the corresponding term root is e081e6... and proposition id is 28f7fb...
Proof:
An exact proof term for the current goal is CD_mul_proj0 {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_minus_CSNo CSNo_conj_CSNo CSNo_add_CSNo CSNo_mul_CSNo.
∎
Theorem. (mul_HSNo_proj1)
∀z w, HSNo z → HSNo w → p1 (mult' z w) = p1 w * p0 z + p1 z * p0 w '
In Proofgold the corresponding term root is a68970... and proposition id is 7821b7...
Proof:
An exact proof term for the current goal is CD_mul_proj1 {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_minus_CSNo CSNo_conj_CSNo CSNo_add_CSNo CSNo_mul_CSNo.
∎
Theorem. (CSNo_HSNo_proj0)
∀x, CSNo x → p0 x = x
In Proofgold the corresponding term root is 60fe35... and proposition id is 7639bd...
Proof:
An exact proof term for the current goal is CD_proj0_F {3} CSNo quaternion_tag_fresh CSNo_0.
∎
Theorem. (CSNo_HSNo_proj1)
∀x, CSNo x → p1 x = 0
In Proofgold the corresponding term root is 15d87b... and proposition id is 952144...
Proof:
An exact proof term for the current goal is CD_proj1_F {3} CSNo quaternion_tag_fresh CSNo_0.
∎
Theorem. (HSNo_p0_0)
p0 0 = 0
In Proofgold the corresponding term root is 6b350d... and proposition id is f0ff58...
Proof:
An exact proof term for the current goal is CSNo_HSNo_proj0 0 CSNo_0.
∎
Theorem. (HSNo_p1_0)
p1 0 = 0
In Proofgold the corresponding term root is ba0409... and proposition id is 1878d5...
Proof:
An exact proof term for the current goal is CSNo_HSNo_proj1 0 CSNo_0.
∎
Theorem. (HSNo_p0_1)
p0 1 = 1
In Proofgold the corresponding term root is 4dd8fa... and proposition id is b0bea3...
Proof:
An exact proof term for the current goal is CSNo_HSNo_proj0 1 CSNo_1.
∎
Theorem. (HSNo_p1_1)
p1 1 = 0
In Proofgold the corresponding term root is 93fc91... and proposition id is 3f14ef...
Proof:
An exact proof term for the current goal is CSNo_HSNo_proj1 1 CSNo_1.
∎
Theorem. (HSNo_p0_i)
p0 i = i
In Proofgold the corresponding term root is 905afa... and proposition id is 50a227...
Proof:
An exact proof term for the current goal is CSNo_HSNo_proj0 i CSNo_Complex_i.
∎
Theorem. (HSNo_p1_i)
p1 i = 0
In Proofgold the corresponding term root is 768a8d... and proposition id is 7ea9df...
Proof:
An exact proof term for the current goal is CSNo_HSNo_proj1 i CSNo_Complex_i.
∎
Theorem. (HSNo_p0_j)
p0 j = 0
In Proofgold the corresponding term root is 767fd7... and proposition id is 21c475...
Proof:
An exact proof term for the current goal is HSNo_proj0_2 0 1 CSNo_0 CSNo_1.
∎
Theorem. (HSNo_p1_j)
p1 j = 1
In Proofgold the corresponding term root is 3b95bd... and proposition id is abaaec...
Proof:
An exact proof term for the current goal is HSNo_proj1_2 0 1 CSNo_0 CSNo_1.
∎
Theorem. (HSNo_p0_k)
p0 k = 0
In Proofgold the corresponding term root is e603b4... and proposition id is 8baec9...
Proof:
An exact proof term for the current goal is HSNo_proj0_2 0 i CSNo_0 CSNo_Complex_i.
∎
Theorem. (HSNo_p1_k)
p1 k = i
In Proofgold the corresponding term root is 80ea56... and proposition id is 575ab4...
Proof:
An exact proof term for the current goal is HSNo_proj1_2 0 i CSNo_0 CSNo_Complex_i.
∎
Theorem. (minus_HSNo_minus_CSNo)
∀x, CSNo x → :-: x = - x
In Proofgold the corresponding term root is a9014c... and proposition id is 7b42d4...
Proof:
An exact proof term for the current goal is CD_minus_F_eq {3} CSNo quaternion_tag_fresh minus_CSNo CSNo_0 minus_CSNo_0.
∎
Theorem. (minus_HSNo_0)
:-: 0 = 0
In Proofgold the corresponding term root is 176f59... and proposition id is 776989...
Proof:
rewrite the current goal using minus_HSNo_minus_CSNo 0 CSNo_0 (from left to right).
An exact proof term for the current goal is minus_CSNo_0.
∎
Theorem. (conj_HSNo_conj_CSNo)
∀x, CSNo x → x '' = x '
In Proofgold the corresponding term root is 64571f... and proposition id is 7817d5...
Proof:
An exact proof term for the current goal is CD_conj_F_eq {3} CSNo quaternion_tag_fresh minus_CSNo CSNo_0 minus_CSNo_0 conj_CSNo.
∎
Theorem. (conj_HSNo_id_SNo)
∀x, SNo x → x '' = x
In Proofgold the corresponding term root is ebe6df... and proposition id is 58d64a...
Proof:
Let x be given.
Assume Hx.
rewrite the current goal using conj_HSNo_conj_CSNo x (SNo_CSNo x Hx) (from left to right).
We will prove x ' = x.
An exact proof term for the current goal is conj_CSNo_id_SNo x Hx.
∎
Theorem. (conj_HSNo_0)
0 '' = 0
In Proofgold the corresponding term root is 0665e6... and proposition id is 1a59ff...
Proof:
rewrite the current goal using conj_HSNo_conj_CSNo 0 CSNo_0 (from left to right).
An exact proof term for the current goal is conj_CSNo_0.
∎
Theorem. (conj_HSNo_1)
1 '' = 1
In Proofgold the corresponding term root is 6faceb... and proposition id is 3cd551...
Proof:
rewrite the current goal using conj_HSNo_conj_CSNo 1 CSNo_1 (from left to right).
An exact proof term for the current goal is conj_CSNo_1.
∎
Theorem. (add_HSNo_add_CSNo)
∀x y, CSNo x → CSNo y → x + y = x + y
In Proofgold the corresponding term root is 6e3971... and proposition id is b05210...
Proof:
An exact proof term for the current goal is CD_add_F_eq {3} CSNo quaternion_tag_fresh add_CSNo CSNo_0 (add_CSNo_0L 0 CSNo_0).
∎
Theorem. (mul_HSNo_mul_CSNo)
∀x y, CSNo x → CSNo y → x ⨯ y = x * y
In Proofgold the corresponding term root is c8a0d0... and proposition id is e84c3f...
Proof:
An exact proof term for the current goal is CD_mul_F_eq {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_0 CSNo_conj_CSNo CSNo_mul_CSNo minus_CSNo_0 add_CSNo_0R mul_CSNo_0L mul_CSNo_0R.
∎
Theorem. (minus_HSNo_invol)
∀z, HSNo z → :-: :-: z = z
In Proofgold the corresponding term root is 91a264... and proposition id is d5104e...
Proof:
An exact proof term for the current goal is CD_minus_invol {3} CSNo quaternion_tag_fresh minus_CSNo CSNo_minus_CSNo minus_CSNo_invol.
∎
Theorem. (conj_HSNo_invol)
∀z, HSNo z → z '' '' = z
In Proofgold the corresponding term root is 8faa1e... and proposition id is 3cc997...
Proof:
An exact proof term for the current goal is CD_conj_invol {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo CSNo_minus_CSNo CSNo_conj_CSNo minus_CSNo_invol conj_CSNo_invol.
∎
Theorem. (conj_minus_HSNo)
∀z, HSNo z → (:-: z) '' = :-: (z '')
In Proofgold the corresponding term root is ad72ab... and proposition id is 97ffd3...
Proof:
An exact proof term for the current goal is CD_conj_minus {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo CSNo_minus_CSNo CSNo_conj_CSNo conj_minus_CSNo.
∎
Theorem. (minus_add_HSNo)
∀z w, HSNo z → HSNo w → :-: (z + w) = :-: z + :-: w
In Proofgold the corresponding term root is ea90cf... and proposition id is 5c75f8...
Proof:
An exact proof term for the current goal is CD_minus_add {3} CSNo quaternion_tag_fresh minus_CSNo add_CSNo CSNo_minus_CSNo CSNo_add_CSNo minus_add_CSNo.
∎
Theorem. (conj_add_HSNo)
∀z w, HSNo z → HSNo w → (z + w) '' = z '' + w ''
In Proofgold the corresponding term root is 777e84... and proposition id is ec65d2...
Proof:
An exact proof term for the current goal is CD_conj_add {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo CSNo_minus_CSNo CSNo_conj_CSNo CSNo_add_CSNo minus_add_CSNo conj_add_CSNo.
∎
Theorem. (add_HSNo_com)
∀z w, HSNo z → HSNo w → z + w = w + z
In Proofgold the corresponding term root is e30f23... and proposition id is a91741...
Proof:
An exact proof term for the current goal is CD_add_com {3} CSNo quaternion_tag_fresh add_CSNo add_CSNo_com.
∎
Theorem. (add_HSNo_assoc)
∀z w v, HSNo z → HSNo w → HSNo v → (z + w) + v = z + (w + v)
In Proofgold the corresponding term root is 2ad3fc... and proposition id is a6a347...
Proof:
Apply CD_add_assoc {3} CSNo quaternion_tag_fresh add_CSNo CSNo_add_CSNo add_CSNo_assoc to the current goal.
∎
Theorem. (add_HSNo_0L)
∀z, HSNo z → add_HSNo 0 z = z
In Proofgold the corresponding term root is 18376d... and proposition id is 1b0119...
Proof:
An exact proof term for the current goal is CD_add_0L {3} CSNo quaternion_tag_fresh add_CSNo CSNo_0 add_CSNo_0L.
∎
Theorem. (add_HSNo_0R)
∀z, HSNo z → add_HSNo z 0 = z
In Proofgold the corresponding term root is 5a9044... and proposition id is 0c0186...
Proof:
An exact proof term for the current goal is CD_add_0R {3} CSNo quaternion_tag_fresh add_CSNo CSNo_0 add_CSNo_0R.
∎
Theorem. (add_HSNo_minus_HSNo_linv)
∀z, HSNo z → add_HSNo (minus_HSNo z) z = 0
In Proofgold the corresponding term root is 2161be... and proposition id is c0a796...
Proof:
An exact proof term for the current goal is CD_add_minus_linv {3} CSNo quaternion_tag_fresh minus_CSNo add_CSNo CSNo_minus_CSNo add_CSNo_minus_CSNo_linv.
∎
Theorem. (add_HSNo_minus_HSNo_rinv)
∀z, HSNo z → add_HSNo z (minus_HSNo z) = 0
In Proofgold the corresponding term root is e16e72... and proposition id is f52141...
Proof:
An exact proof term for the current goal is CD_add_minus_rinv {3} CSNo quaternion_tag_fresh minus_CSNo add_CSNo CSNo_minus_CSNo add_CSNo_minus_CSNo_rinv.
∎
Theorem. (mul_HSNo_0R)
∀z, HSNo z → z ⨯ 0 = 0
In Proofgold the corresponding term root is c6c5df... and proposition id is a6c3c2...
Proof:
An exact proof term for the current goal is CD_mul_0R {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_0 minus_CSNo_0 conj_CSNo_0 (add_CSNo_0L 0 CSNo_0) mul_CSNo_0L mul_CSNo_0R.
∎
Theorem. (mul_HSNo_0L)
∀z, HSNo z → 0 ⨯ z = 0
In Proofgold the corresponding term root is d9f510... and proposition id is 2984ec...
Proof:
An exact proof term for the current goal is CD_mul_0L {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_0 CSNo_conj_CSNo minus_CSNo_0 (add_CSNo_0L 0 CSNo_0) mul_CSNo_0L mul_CSNo_0R.
∎
Theorem. (mul_HSNo_1R)
∀z, HSNo z → z ⨯ 1 = z
In Proofgold the corresponding term root is ec38b4... and proposition id is 896e80...
Proof:
An exact proof term for the current goal is CD_mul_1R {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_0 CSNo_1 minus_CSNo_0 conj_CSNo_0 conj_CSNo_1 add_CSNo_0L add_CSNo_0R mul_CSNo_0L mul_CSNo_1R.
∎
Theorem. (mul_HSNo_1L)
∀z, HSNo z → 1 ⨯ z = z
In Proofgold the corresponding term root is 80a90e... and proposition id is 4c64b4...
Proof:
An exact proof term for the current goal is CD_mul_1L {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_0 CSNo_1 CSNo_conj_CSNo minus_CSNo_0 add_CSNo_0R mul_CSNo_0L mul_CSNo_0R mul_CSNo_1L mul_CSNo_1R.
∎
Theorem. (conj_mul_HSNo)
∀z w, HSNo z → HSNo w → (z ⨯ w) '' = w '' ⨯ z ''
In Proofgold the corresponding term root is 64a2e5... and proposition id is 225be1...
Proof:
An exact proof term for the current goal is CD_conj_mul {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_minus_CSNo CSNo_conj_CSNo CSNo_add_CSNo CSNo_mul_CSNo minus_CSNo_invol conj_CSNo_invol conj_minus_CSNo conj_add_CSNo minus_add_CSNo add_CSNo_com conj_mul_CSNo minus_mul_CSNo_distrR minus_mul_CSNo_distrL.
∎
Theorem. (mul_HSNo_distrL)
∀z w u, HSNo z → HSNo w → HSNo u → z ⨯ (w + u) = z ⨯ w + z ⨯ u
In Proofgold the corresponding term root is 347c37... and proposition id is 0d4990...
Proof:
An exact proof term for the current goal is CD_add_mul_distrL {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_minus_CSNo CSNo_conj_CSNo CSNo_add_CSNo CSNo_mul_CSNo minus_add_CSNo conj_add_CSNo add_CSNo_assoc add_CSNo_com mul_CSNo_distrL mul_CSNo_distrR.
∎
Theorem. (mul_HSNo_distrR)
∀z w u, HSNo z → HSNo w → HSNo u → (z + w) ⨯ u = z ⨯ u + w ⨯ u
In Proofgold the corresponding term root is c716fd... and proposition id is 7dee08...
Proof:
An exact proof term for the current goal is CD_add_mul_distrR {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_minus_CSNo CSNo_conj_CSNo CSNo_add_CSNo CSNo_mul_CSNo minus_add_CSNo add_CSNo_assoc add_CSNo_com mul_CSNo_distrL mul_CSNo_distrR.
∎
Theorem. (minus_mul_HSNo_distrR)
∀z w, HSNo z → HSNo w → z ⨯ (:-: w) = :-: z ⨯ w
In Proofgold the corresponding term root is e18e00... and proposition id is 122e5c...
Proof:
An exact proof term for the current goal is CD_minus_mul_distrR {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_minus_CSNo CSNo_conj_CSNo CSNo_add_CSNo CSNo_mul_CSNo conj_minus_CSNo minus_add_CSNo minus_mul_CSNo_distrR minus_mul_CSNo_distrL.
∎
Theorem. (minus_mul_HSNo_distrL)
∀z w, HSNo z → HSNo w → (:-: z) ⨯ w = :-: z ⨯ w
In Proofgold the corresponding term root is e48f25... and proposition id is e67e13...
Proof:
An exact proof term for the current goal is CD_minus_mul_distrL {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_minus_CSNo CSNo_conj_CSNo CSNo_add_CSNo CSNo_mul_CSNo minus_add_CSNo minus_mul_CSNo_distrR minus_mul_CSNo_distrL.
∎
Theorem. (exp_HSNo_nat_0)
∀z, z0 = 1
In Proofgold the corresponding term root is a8e4e1... and proposition id is 858195...
Proof:
An exact proof term for the current goal is CD_exp_nat_0 {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo.
∎
Theorem. (exp_HSNo_nat_S)
∀z n, nat_p n → z(ordsucc n) = z ⨯ zn
In Proofgold the corresponding term root is 5c2375... and proposition id is 5ccd45...
Proof:
An exact proof term for the current goal is CD_exp_nat_S {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo.
∎
Theorem. (exp_HSNo_nat_1)
∀z, HSNo z → z1 = z
In Proofgold the corresponding term root is 83d5ec... and proposition id is 209eff...
Proof:
An exact proof term for the current goal is CD_exp_nat_1 {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_0 CSNo_1 minus_CSNo_0 conj_CSNo_0 conj_CSNo_1 add_CSNo_0L add_CSNo_0R mul_CSNo_0L mul_CSNo_1R.
∎
Theorem. (exp_HSNo_nat_2)
∀z, HSNo z → z2 = z ⨯ z
In Proofgold the corresponding term root is 0756a0... and proposition id is dd7b0e...
Proof:
An exact proof term for the current goal is CD_exp_nat_2 {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_0 CSNo_1 minus_CSNo_0 conj_CSNo_0 conj_CSNo_1 add_CSNo_0L add_CSNo_0R mul_CSNo_0L mul_CSNo_1R.
∎
Theorem. (HSNo_exp_HSNo_nat)
∀z, HSNo z → ∀n, nat_p n → HSNo (zn)
In Proofgold the corresponding term root is dfb84a... and proposition id is cfcd35...
Proof:
An exact proof term for the current goal is CD_exp_nat_CD {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_minus_CSNo CSNo_conj_CSNo CSNo_add_CSNo CSNo_mul_CSNo CSNo_0 CSNo_1.
∎
Theorem. (add_CSNo_com_3b_1_2)
∀x y z, CSNo x → CSNo y → CSNo z → (x + y) + z = (x + z) + y
In Proofgold the corresponding term root is e361b0... and proposition id is 4b207f...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
We will prove (x + y) + z = (x + z) + y.
rewrite the current goal using add_CSNo_assoc x y z Hx Hy Hz (from left to right).
We will prove x + y + z = (x + z) + y.
rewrite the current goal using add_CSNo_assoc x z y Hx Hz Hy (from left to right).
We will prove x + y + z = x + z + y.
Use f_equal.
An exact proof term for the current goal is add_CSNo_com y z Hy Hz.
∎
Theorem. (add_CSNo_com_4_inner_mid)
∀x y z w, CSNo x → CSNo y → CSNo z → CSNo w → (x + y) + (z + w) = (x + z) + (y + w)
In Proofgold the corresponding term root is 458601... and proposition id is fbf900...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
rewrite the current goal using add_CSNo_assoc (x + y) z w (CSNo_add_CSNo 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 add_CSNo_com_3b_1_2 x y z Hx Hy Hz (from left to right).
We will prove ((x + z) + y) + w = (x + z) + (y + w).
An exact proof term for the current goal is add_CSNo_assoc (x + z) y w (CSNo_add_CSNo x z Hx Hz) Hy Hw.
∎
Theorem. (add_CSNo_rotate_4_0312)
∀x y z w, CSNo x → CSNo y → CSNo z → CSNo w → (x + y) + (z + w) = (x + w) + (y + z)
In Proofgold the corresponding term root is fbee7e... and proposition id is 6a0798...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
rewrite the current goal using add_CSNo_com z w Hz Hw (from left to right).
We will prove (x + y) + (w + z) = (x + w) + (y + z).
An exact proof term for the current goal is add_CSNo_com_4_inner_mid x y w z Hx Hy Hw Hz.
∎
Theorem. (Quaternion_i_sqr)
i ⨯ i = :-: 1
In Proofgold the corresponding term root is ab7a70... and proposition id is 6ce0c7...
Proof:
rewrite the current goal using mul_HSNo_mul_CSNo i i CSNo_Complex_i CSNo_Complex_i (from left to right).
rewrite the current goal using minus_HSNo_minus_CSNo 1 CSNo_1 (from left to right).
We will prove i * i = - 1.
An exact proof term for the current goal is Complex_i_sqr.
∎
Theorem. (Quaternion_j_sqr)
j ⨯ j = :-: 1
In Proofgold the corresponding term root is b4236f... and proposition id is 9f0956...
Proof:
We prove the intermediate claim Ljj: HSNo (j ⨯ j).
An exact proof term for the current goal is HSNo_mul_HSNo j j HSNo_Quaternion_j HSNo_Quaternion_j.
We prove the intermediate claim Lm1: HSNo (:-: 1).
An exact proof term for the current goal is HSNo_minus_HSNo 1 HSNo_1.
Apply HSNo_proj0proj1_split (j ⨯ j) (:-: 1) Ljj Lm1 to the current goal.
We will prove p0 (j ⨯ j) = p0 (:-: 1).
rewrite the current goal using mul_HSNo_proj0 j j HSNo_Quaternion_j HSNo_Quaternion_j (from left to right).
rewrite the current goal using minus_HSNo_proj0 1 HSNo_1 (from left to right).
We will prove p0 j * p0 j + - p1 j ' * p1 j = - p0 1.
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
rewrite the current goal using CSNo_HSNo_proj0 1 CSNo_1 (from left to right).
We will prove 0 * 0 + - 1 ' * 1 = - 1.
rewrite the current goal using conj_CSNo_1 (from left to right).
rewrite the current goal using mul_CSNo_0L 0 CSNo_0 (from left to right).
rewrite the current goal using mul_CSNo_1L 1 CSNo_1 (from left to right).
We will prove 0 + - 1 = - 1.
An exact proof term for the current goal is add_CSNo_0L (- 1) (CSNo_minus_CSNo 1 CSNo_1).
We will prove p1 (j ⨯ j) = p1 (:-: 1).
rewrite the current goal using mul_HSNo_proj1 j j HSNo_Quaternion_j HSNo_Quaternion_j (from left to right).
rewrite the current goal using minus_HSNo_proj1 1 HSNo_1 (from left to right).
We will prove p1 j * p0 j + p1 j * p0 j ' = - p1 1.
rewrite the current goal using HSNo_p1_1 (from left to right).
rewrite the current goal using minus_CSNo_0 (from left to right).
We will prove p1 j * p0 j + p1 j * p0 j ' = 0.
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
We will prove 1 * 0 + 1 * 0 ' = 0.
rewrite the current goal using conj_CSNo_0 (from left to right).
We will prove 1 * 0 + 1 * 0 = 0.
rewrite the current goal using mul_CSNo_0R 1 CSNo_1 (from left to right).
An exact proof term for the current goal is add_CSNo_0L 0 CSNo_0.
∎
Theorem. (Quaternion_k_sqr)
k ⨯ k = :-: 1
In Proofgold the corresponding term root is 0298ee... and proposition id is c4384d...
Proof:
We prove the intermediate claim Lkk: HSNo (k ⨯ k).
An exact proof term for the current goal is HSNo_mul_HSNo k k HSNo_Quaternion_k HSNo_Quaternion_k.
We prove the intermediate claim Lm1: HSNo (:-: 1).
An exact proof term for the current goal is HSNo_minus_HSNo 1 HSNo_1.
Apply HSNo_proj0proj1_split (k ⨯ k) (:-: 1) Lkk Lm1 to the current goal.
We will prove p0 (k ⨯ k) = p0 (:-: 1).
rewrite the current goal using mul_HSNo_proj0 k k HSNo_Quaternion_k HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_HSNo_proj0 1 HSNo_1 (from left to right).
We will prove p0 k * p0 k + - p1 k ' * p1 k = - p0 1.
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
rewrite the current goal using CSNo_HSNo_proj0 1 CSNo_1 (from left to right).
We will prove 0 * 0 + - i ' * i = - 1.
rewrite the current goal using mul_CSNo_0L 0 CSNo_0 (from left to right).
rewrite the current goal using conj_CSNo_i (from left to right).
We will prove 0 + - (- i) * i = - 1.
rewrite the current goal using minus_mul_CSNo_distrL (- i) i (CSNo_minus_CSNo i CSNo_Complex_i) CSNo_Complex_i (from right to left).
We will prove 0 + (- - i) * i = - 1.
rewrite the current goal using minus_CSNo_invol i CSNo_Complex_i (from left to right).
We will prove 0 + i * i = - 1.
rewrite the current goal using Complex_i_sqr (from left to right).
We will prove 0 + - 1 = - 1.
An exact proof term for the current goal is add_CSNo_0L (- 1) (CSNo_minus_CSNo 1 CSNo_1).
We will prove p1 (k ⨯ k) = p1 (:-: 1).
rewrite the current goal using mul_HSNo_proj1 k k HSNo_Quaternion_k HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_HSNo_proj1 1 HSNo_1 (from left to right).
We will prove p1 k * p0 k + p1 k * p0 k ' = - p1 1.
rewrite the current goal using HSNo_p1_1 (from left to right).
rewrite the current goal using minus_CSNo_0 (from left to right).
We will prove p1 k * p0 k + p1 k * p0 k ' = 0.
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
We will prove i * 0 + i * 0 ' = 0.
rewrite the current goal using conj_CSNo_0 (from left to right).
We will prove i * 0 + i * 0 = 0.
rewrite the current goal using mul_CSNo_0R i CSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_CSNo_0L 0 CSNo_0.
∎
Theorem. (Quaternion_i_j)
i ⨯ j = k
In Proofgold the corresponding term root is 0337aa... and proposition id is b64eb9...
Proof:
We prove the intermediate claim Lij: HSNo (i ⨯ j).
An exact proof term for the current goal is HSNo_mul_HSNo i j HSNo_Complex_i HSNo_Quaternion_j.
Apply HSNo_proj0proj1_split (i ⨯ j) k Lij HSNo_Quaternion_k to the current goal.
We will prove p0 (i ⨯ j) = p0 k.
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using mul_HSNo_proj0 i j HSNo_Complex_i HSNo_Quaternion_j (from left to right).
We will prove p0 i * p0 j + - (p1 j ' * p1 i) = 0.
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using HSNo_p1_i (from left to right).
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
We will prove i * 0 + - (1 ' * 0) = 0.
rewrite the current goal using mul_CSNo_0R i CSNo_Complex_i (from left to right).
rewrite the current goal using mul_CSNo_0R (1 ') (CSNo_conj_CSNo 1 CSNo_1) (from left to right).
We will prove 0 + - 0 = 0.
rewrite the current goal using minus_CSNo_0 (from left to right).
An exact proof term for the current goal is add_CSNo_0L 0 CSNo_0.
We will prove p1 (i ⨯ j) = p1 k.
rewrite the current goal using HSNo_p1_k (from left to right).
rewrite the current goal using mul_HSNo_proj1 i j HSNo_Complex_i HSNo_Quaternion_j (from left to right).
We will prove p1 j * p0 i + p1 i * p0 j ' = i.
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using HSNo_p1_i (from left to right).
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
We will prove 1 * i + 0 * 0 ' = i.
rewrite the current goal using mul_CSNo_1L i CSNo_Complex_i (from left to right).
rewrite the current goal using mul_CSNo_0L (0 ') (CSNo_conj_CSNo 0 CSNo_0) (from left to right).
We will prove i + 0 = i.
An exact proof term for the current goal is add_CSNo_0R i CSNo_Complex_i.
∎
Theorem. (Quaternion_j_k)
j ⨯ k = i
In Proofgold the corresponding term root is 4089fd... and proposition id is 2d01eb...
Proof:
We prove the intermediate claim Ljk: HSNo (j ⨯ k).
An exact proof term for the current goal is HSNo_mul_HSNo j k HSNo_Quaternion_j HSNo_Quaternion_k.
Apply HSNo_proj0proj1_split (j ⨯ k) i Ljk HSNo_Complex_i to the current goal.
We will prove p0 (j ⨯ k) = p0 i.
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using mul_HSNo_proj0 j k HSNo_Quaternion_j HSNo_Quaternion_k (from left to right).
We will prove p0 j * p0 k + - (p1 k ' * p1 j) = i.
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
We will prove 0 * 0 + - (i ' * 1) = i.
rewrite the current goal using mul_CSNo_0R 0 CSNo_0 (from left to right).
rewrite the current goal using mul_CSNo_1R (i ') (CSNo_conj_CSNo i CSNo_Complex_i) (from left to right).
We will prove 0 + - (i ') = i.
rewrite the current goal using conj_CSNo_i (from left to right).
We will prove 0 + - - i = i.
rewrite the current goal using minus_CSNo_invol i CSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_CSNo_0L i CSNo_Complex_i.
We will prove p1 (j ⨯ k) = p1 i.
rewrite the current goal using HSNo_p1_i (from left to right).
rewrite the current goal using mul_HSNo_proj1 j k HSNo_Quaternion_j HSNo_Quaternion_k (from left to right).
We will prove p1 k * p0 j + p1 j * p0 k ' = 0.
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
We will prove i * 0 + 1 * 0 ' = 0.
rewrite the current goal using conj_CSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_CSNo_0R i CSNo_Complex_i (from left to right).
rewrite the current goal using mul_CSNo_0R 1 CSNo_1 (from left to right).
An exact proof term for the current goal is add_CSNo_0R 0 CSNo_0.
∎
Theorem. (Quaternion_k_i)
k ⨯ i = j
In Proofgold the corresponding term root is 7fb308... and proposition id is da5ded...
Proof:
We prove the intermediate claim Lki: HSNo (k ⨯ i).
An exact proof term for the current goal is HSNo_mul_HSNo k i HSNo_Quaternion_k HSNo_Complex_i.
Apply HSNo_proj0proj1_split (k ⨯ i) j Lki HSNo_Quaternion_j to the current goal.
We will prove p0 (k ⨯ i) = p0 j.
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using mul_HSNo_proj0 k i HSNo_Quaternion_k HSNo_Complex_i (from left to right).
We will prove p0 k * p0 i + - (p1 i ' * p1 k) = 0.
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using HSNo_p1_i (from left to right).
We will prove 0 * i + - (0 ' * i) = 0.
rewrite the current goal using conj_CSNo_id_SNo 0 SNo_0 (from left to right).
We will prove 0 * i + - (0 * i) = 0.
rewrite the current goal using mul_CSNo_0L i CSNo_Complex_i (from left to right).
We will prove 0 + - 0 = 0.
rewrite the current goal using minus_CSNo_0 (from left to right).
An exact proof term for the current goal is add_CSNo_0R 0 CSNo_0.
We will prove p1 (k ⨯ i) = p1 j.
rewrite the current goal using HSNo_p1_j (from left to right).
rewrite the current goal using mul_HSNo_proj1 k i HSNo_Quaternion_k HSNo_Complex_i (from left to right).
We will prove p1 i * p0 k + p1 k * p0 i ' = 1.
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using HSNo_p1_i (from left to right).
We will prove 0 * 0 + i * (i ') = 1.
rewrite the current goal using mul_CSNo_0L 0 CSNo_0 (from left to right).
rewrite the current goal using conj_CSNo_i (from left to right).
We will prove 0 + i * (- i) = 1.
rewrite the current goal using minus_mul_CSNo_distrR i i CSNo_Complex_i CSNo_Complex_i (from left to right).
We will prove 0 + - i * i = 1.
rewrite the current goal using Complex_i_sqr (from left to right).
We will prove 0 + - - 1 = 1.
rewrite the current goal using minus_CSNo_invol 1 CSNo_1 (from left to right).
An exact proof term for the current goal is add_CSNo_0L 1 CSNo_1.
∎
Theorem. (Quaternion_j_i)
j ⨯ i = :-: k
In Proofgold the corresponding term root is 134bae... and proposition id is 411eda...
Proof:
We prove the intermediate claim Lji: HSNo (j ⨯ i).
An exact proof term for the current goal is HSNo_mul_HSNo j i HSNo_Quaternion_j HSNo_Complex_i.
Apply HSNo_proj0proj1_split (j ⨯ i) (:-: k) Lji (HSNo_minus_HSNo k HSNo_Quaternion_k) to the current goal.
We will prove p0 (j ⨯ i) = p0 (:-: k).
rewrite the current goal using minus_HSNo_proj0 k HSNo_Quaternion_k (from left to right).
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using mul_HSNo_proj0 j i HSNo_Quaternion_j HSNo_Complex_i (from left to right).
We will prove p0 j * p0 i + - (p1 i ' * p1 j) = - 0.
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using HSNo_p1_i (from left to right).
We will prove 0 * i + - (0 ' * 1) = - 0.
rewrite the current goal using conj_CSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using mul_CSNo_0L i CSNo_Complex_i (from left to right).
rewrite the current goal using mul_CSNo_0L 1 CSNo_1 (from left to right).
We will prove 0 + - 0 = - 0.
An exact proof term for the current goal is add_CSNo_0L (- 0) (CSNo_minus_CSNo 0 CSNo_0).
We will prove p1 (j ⨯ i) = p1 (:-: k).
rewrite the current goal using minus_HSNo_proj1 k HSNo_Quaternion_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
rewrite the current goal using mul_HSNo_proj1 j i HSNo_Quaternion_j HSNo_Complex_i (from left to right).
We will prove p1 i * p0 j + p1 j * p0 i ' = - i.
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using HSNo_p1_i (from left to right).
We will prove 0 * 0 + 1 * i ' = - i.
rewrite the current goal using mul_CSNo_0R 0 CSNo_0 (from left to right).
rewrite the current goal using mul_CSNo_1L (i ') (CSNo_conj_CSNo i CSNo_Complex_i) (from left to right).
rewrite the current goal using conj_CSNo_i (from left to right).
We will prove 0 + - i = - i.
An exact proof term for the current goal is add_CSNo_0L (- i) (CSNo_minus_CSNo i CSNo_Complex_i).
∎
Theorem. (Quaternion_k_j)
k ⨯ j = :-: i
In Proofgold the corresponding term root is a2b355... and proposition id is 80ed56...
Proof:
We prove the intermediate claim Lkj: HSNo (k ⨯ j).
An exact proof term for the current goal is HSNo_mul_HSNo k j HSNo_Quaternion_k HSNo_Quaternion_j.
Apply HSNo_proj0proj1_split (k ⨯ j) (:-: i) Lkj (HSNo_minus_HSNo i HSNo_Complex_i) to the current goal.
We will prove p0 (k ⨯ j) = p0 (:-: i).
rewrite the current goal using minus_HSNo_proj0 i HSNo_Complex_i (from left to right).
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using mul_HSNo_proj0 k j HSNo_Quaternion_k HSNo_Quaternion_j (from left to right).
We will prove p0 k * p0 j + - (p1 j ' * p1 k) = - i.
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
We will prove 0 * 0 + - (1 ' * i) = - i.
rewrite the current goal using mul_CSNo_0R 0 CSNo_0 (from left to right).
rewrite the current goal using conj_CSNo_id_SNo 1 SNo_1 (from left to right).
rewrite the current goal using mul_CSNo_1L i CSNo_Complex_i (from left to right).
We will prove 0 + - i = - i.
An exact proof term for the current goal is add_CSNo_0L (- i) (CSNo_minus_CSNo i CSNo_Complex_i).
We will prove p1 (k ⨯ j) = p1 (:-: i).
rewrite the current goal using minus_HSNo_proj1 i HSNo_Complex_i (from left to right).
rewrite the current goal using HSNo_p1_i (from left to right).
rewrite the current goal using mul_HSNo_proj1 k j HSNo_Quaternion_k HSNo_Quaternion_j (from left to right).
We will prove p1 j * p0 k + p1 k * p0 j ' = - 0.
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
We will prove 1 * 0 + i * 0 ' = - 0.
rewrite the current goal using conj_CSNo_id_SNo 0 SNo_0 (from left to right).
rewrite the current goal using minus_CSNo_0 (from left to right).
rewrite the current goal using mul_CSNo_0R 1 CSNo_1 (from left to right).
rewrite the current goal using mul_CSNo_0R i CSNo_Complex_i (from left to right).
An exact proof term for the current goal is add_CSNo_0R 0 CSNo_0.
∎
Theorem. (Quaternion_i_k)
i ⨯ k = :-: j
In Proofgold the corresponding term root is 987b31... and proposition id is 0343db...
Proof:
We prove the intermediate claim Lik: HSNo (i ⨯ k).
An exact proof term for the current goal is HSNo_mul_HSNo i k HSNo_Complex_i HSNo_Quaternion_k.
Apply HSNo_proj0proj1_split (i ⨯ k) (:-: j) Lik (HSNo_minus_HSNo j HSNo_Quaternion_j) to the current goal.
We will prove p0 (i ⨯ k) = p0 (:-: j).
rewrite the current goal using minus_HSNo_proj0 j HSNo_Quaternion_j (from left to right).
rewrite the current goal using HSNo_p0_j (from left to right).
rewrite the current goal using mul_HSNo_proj0 i k HSNo_Complex_i HSNo_Quaternion_k (from left to right).
We will prove p0 i * p0 k + - (p1 k ' * p1 i) = - 0.
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using HSNo_p1_i (from left to right).
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
We will prove i * 0 + - (i ' * 0) = - 0.
rewrite the current goal using mul_CSNo_0R i CSNo_Complex_i (from left to right).
rewrite the current goal using mul_CSNo_0R (i ') (CSNo_conj_CSNo i CSNo_Complex_i) (from left to right).
We will prove 0 + - 0 = - 0.
An exact proof term for the current goal is add_CSNo_0L (- 0) (CSNo_minus_CSNo 0 CSNo_0).
We will prove p1 (i ⨯ k) = p1 (:-: j).
rewrite the current goal using minus_HSNo_proj1 j HSNo_Quaternion_j (from left to right).
rewrite the current goal using HSNo_p1_j (from left to right).
rewrite the current goal using mul_HSNo_proj1 i k HSNo_Complex_i HSNo_Quaternion_k (from left to right).
We will prove p1 k * p0 i + p1 i * p0 k ' = - 1.
rewrite the current goal using HSNo_p0_i (from left to right).
rewrite the current goal using HSNo_p1_i (from left to right).
rewrite the current goal using HSNo_p0_k (from left to right).
rewrite the current goal using HSNo_p1_k (from left to right).
We will prove i * i + 0 * 0 ' = - 1.
rewrite the current goal using mul_CSNo_0L (0 ') (CSNo_conj_CSNo 0 CSNo_0) (from left to right).
rewrite the current goal using Complex_i_sqr (from left to right).
We will prove - 1 + 0 = - 1.
An exact proof term for the current goal is add_CSNo_0R (- 1) (CSNo_minus_CSNo 1 CSNo_1).
∎
Theorem. (add_CSNo_rotate_3_1)
∀x y z, CSNo x → CSNo y → CSNo z → x + y + z = z + x + y
In Proofgold the corresponding term root is ef39c1... and proposition id is 271f1c...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
We will prove x + (y + z) = z + (x + y).
Use transitivity with x + (z + y), (x + z) + y, and (z + x) + y.
Use f_equal.
An exact proof term for the current goal is add_CSNo_com y z Hy Hz.
Use symmetry.
An exact proof term for the current goal is add_CSNo_assoc x z y Hx Hz Hy.
Use f_equal.
An exact proof term for the current goal is add_CSNo_com x z Hx Hz.
An exact proof term for the current goal is add_CSNo_assoc z x y Hz Hx Hy.
∎
Theorem. (mul_CSNo_rotate_3_1)
∀x y z, CSNo x → CSNo y → CSNo z → x * y * z = z * x * y
In Proofgold the corresponding term root is caf07e... and proposition id is 0a85fc...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
We will prove x * (y * z) = z * (x * y).
Use transitivity with x * (z * y), (x * z) * y, and (z * x) * y.
Use f_equal.
An exact proof term for the current goal is mul_CSNo_com y z Hy Hz.
An exact proof term for the current goal is mul_CSNo_assoc x z y Hx Hz Hy.
Use f_equal.
An exact proof term for the current goal is mul_CSNo_com x z Hx Hz.
Use symmetry.
An exact proof term for the current goal is mul_CSNo_assoc z x y Hz Hx Hy.
∎
Theorem. (mul_HSNo_assoc)
∀z w v, HSNo z → HSNo w → HSNo v → z ⨯ (w ⨯ v) = (z ⨯ w) ⨯ v
In Proofgold the corresponding term root is 75e0e2... and proposition id is 980dee...
Proof:
Let z, w and v be given.
Assume Hz Hw Hv.
We prove the intermediate claim Lwv: HSNo (mult' w v).
An exact proof term for the current goal is HSNo_mul_HSNo w v Hw Hv.
We prove the intermediate claim Lzw: HSNo (mult' z w).
An exact proof term for the current goal is HSNo_mul_HSNo z w Hz Hw.
We prove the intermediate claim Lzwv1: HSNo (mult' z (mult' w v)).
An exact proof term for the current goal is HSNo_mul_HSNo z (mult' w v) Hz Lwv.
We prove the intermediate claim Lzwv2: HSNo (mult' (mult' z w) v).
An exact proof term for the current goal is HSNo_mul_HSNo (mult' z w) v Lzw Hv.
We prove the intermediate claim Lp0zR: CSNo (p0 z).
An exact proof term for the current goal is HSNo_proj0R z Hz.
We prove the intermediate claim Lp0wR: CSNo (p0 w).
An exact proof term for the current goal is HSNo_proj0R w Hw.
We prove the intermediate claim Lp0vR: CSNo (p0 v).
An exact proof term for the current goal is HSNo_proj0R v Hv.
We prove the intermediate claim Lp1zR: CSNo (p1 z).
An exact proof term for the current goal is HSNo_proj1R z Hz.
We prove the intermediate claim Lp1wR: CSNo (p1 w).
An exact proof term for the current goal is HSNo_proj1R w Hw.
We prove the intermediate claim Lp1vR: CSNo (p1 v).
An exact proof term for the current goal is HSNo_proj1R v Hv.
We prove the intermediate claim L1: CSNo (p0 w ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L2: CSNo (p1 w ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L3: CSNo (p1 v ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L4: CSNo (p0 v ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L5: CSNo (p0 v ' ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L6: CSNo (p1 w ' ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L7: CSNo (p1 w * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L8: CSNo (p0 z * p0 w).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L9: CSNo (p0 w * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L10: CSNo (p0 w * p0 v).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L11: CSNo (p1 v * p0 w).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L12: CSNo ((p1 v * p0 w) ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L13: CSNo ((p0 w * p0 v) ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L14: CSNo (p1 z * p0 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L15: CSNo (p0 z * p0 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L16: CSNo (p0 v ' * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L17: CSNo (p1 v * p1 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L18: CSNo (p1 v ' * p1 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L19: CSNo (p1 w ' * p1 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L20: CSNo (p1 v ' * p1 w).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L21: CSNo (p1 w * p0 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L22: CSNo (p0 w ' * p1 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L23: CSNo (p0 v ' ' * p1 w).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L24: CSNo ((p1 w * p0 v ') ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L25: CSNo ((p1 v ' * p1 w) ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L26: CSNo (- p1 w ' * p1 z).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L27: CSNo (p0 w ' * p0 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L28: CSNo (p0 v ' * p0 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L29: CSNo (- p1 v ' * p1 w).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L30: CSNo (p1 w ' * p1 w ' ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L31: CSNo ((- p1 v ' * p1 w) ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L32: CSNo (p1 v * p0 z * p0 w).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L33: CSNo (p1 v * p0 w * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L34: CSNo (p0 z * p0 w * p0 v).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L35: CSNo (- (p1 v ' * p1 w) ').
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L36: CSNo (p1 v * p1 w ' * p1 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L37: CSNo (p1 w * p0 z * p0 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L38: CSNo (p1 w * p0 v ' * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L39: CSNo (p1 z * p1 v * p1 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L40: CSNo (p0 z * p1 v ' * p1 w).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L41: CSNo (p0 v * p1 w ' * p1 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L42: CSNo (- p1 v * p1 w ' * p1 z).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L43: CSNo (p1 z * p0 w ' * p0 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L44: CSNo (p1 z * p0 v ' * p0 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L45: CSNo (- p1 z * p1 v * p1 w ').
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L46: CSNo (- p0 z * p1 v ' * p1 w).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L47: CSNo (p0 w ' * p1 v ' * p1 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L48: CSNo (- p0 v * p1 w ' * p1 z).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L49: CSNo (- p0 w ' * p1 v ' * p1 z).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L50: CSNo (p1 w * p0 z + p1 z * p0 w ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L51: CSNo (p1 v * p0 w + p1 w * p0 v ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L52: CSNo (p0 z * p0 w + - p1 w ' * p1 z).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L53: CSNo (p0 w * p0 v + - p1 v ' * p1 w).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L54: CSNo ((p1 v * p0 w + p1 w * p0 v ') ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L55: CSNo ((p0 w * p0 v + - p1 v ' * p1 w) ').
Apply CSNo_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L56: CSNo (p0 w ' * p1 v ' + p0 v ' ' * p1 w).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L57: CSNo ((p1 v * p0 w) ' + (p1 w * p0 v ') ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L58: CSNo ((p1 v * p0 w + p1 w * p0 v ') * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L59: CSNo (p0 v ' * p0 w ' + - (p1 v ' * p1 w) ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L60: CSNo ((p0 w * p0 v) ' + (- p1 v ' * p1 w) ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L61: CSNo (p1 v * (p0 z * p0 w + - p1 w ' * p1 z)).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L62: CSNo ((p1 w * p0 z + p1 z * p0 w ') * p0 v ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L63: CSNo (p0 z * (p0 w * p0 v + - p1 v ' * p1 w)).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L64: CSNo ((p1 v * p0 w + p1 w * p0 v ') ' * p1 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L65: CSNo (p1 z * (p0 w * p0 v + - p1 v ' * p1 w) ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L66: CSNo (- (p1 v * p0 w + p1 w * p0 v ') ' * p1 z).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L67: CSNo (p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L68: CSNo (p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L69: CSNo (- p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L70: CSNo (- p1 v * p1 w ' * p1 z + p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L71: CSNo (p1 w * p0 v ' * p0 z + p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L72: CSNo (- p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L73: CSNo (p1 v * (p0 z * p0 w + - p1 w ' * p1 z) + (p1 w * p0 z + p1 z * p0 w ') * p0 v ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L74: CSNo ((p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 w * p0 v + - p1 v ' * p1 w) ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L75: CSNo (p0 z * (p0 w * p0 v + - p1 v ' * p1 w) + - (p1 v * p0 w + p1 w * p0 v ') ' * p1 z).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L76: CSNo (p1 v * p0 z * p0 w + - p1 v * p1 w ' * p1 z + p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L77: CSNo (p1 v * p0 w * p0 z + p1 w * p0 v ' * p0 z + p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L78: CSNo (p0 z * p0 w * p0 v + - p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z).
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L79: CSNo (p0 v * p1 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L80: CSNo (p1 z * p0 v).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L81: CSNo (p1 w ' * p1 z * p0 v).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L82: CSNo (- p1 w ' * p1 z * p0 v).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L83: CSNo (p1 v ' * p1 w * p0 z).
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L84: CSNo (p1 v ' * p1 z * p0 w ').
Apply CSNo_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L85: CSNo (- p1 v ' * p1 w * p0 z).
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L86: CSNo (- p1 v ' * p1 z * p0 w ').
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L87: CSNo (- p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L88: CSNo (- p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w ').
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
We prove the intermediate claim L89: CSNo (- p1 v ').
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
We prove the intermediate claim L90: CSNo (- p1 v * p1 w ').
Apply CSNo_minus_CSNo to the current goal.
An exact proof term for the current goal is ??.
Apply HSNo_proj0proj1_split (mult' z (mult' w v)) (mult' (mult' z w) v) Lzwv1 Lzwv2 to the current goal.
We will prove p0 (mult' z (mult' w v)) = p0 (mult' (mult' z w) v).
Use transitivity with p0 z * p0 (mult' w v) + - p1 (mult' w v) ' * p1 z, p0 z * (p0 w * p0 v + - p1 v ' * p1 w) + - (p1 v * p0 w + p1 w * p0 v ') ' * p1 z, p0 z * p0 w * p0 v + - p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z, p0 z * p0 w * p0 v + - p1 w ' * p1 z * p0 v + - p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w ', (p0 z * p0 w + - p1 w ' * p1 z) * p0 v + - p1 v ' * (p1 w * p0 z + p1 z * p0 w '), and p0 (mult' z w) * p0 v + - p1 v ' * p1 (mult' z w).
An exact proof term for the current goal is mul_HSNo_proj0 z (mult' w v) Hz Lwv.
We will prove p0 z * p0 (mult' w v) + - p1 (mult' w v) ' * p1 z = p0 z * (p0 w * p0 v + - p1 v ' * p1 w) + - (p1 v * p0 w + p1 w * p0 v ') ' * p1 z.
Use f_equal.
Use f_equal.
An exact proof term for the current goal is mul_HSNo_proj0 w v Hw Hv.
Use f_equal.
Use f_equal.
Use f_equal.
An exact proof term for the current goal is mul_HSNo_proj1 w v Hw Hv.
We will prove p0 z * (p0 w * p0 v + - p1 v ' * p1 w) + - (p1 v * p0 w + p1 w * p0 v ') ' * p1 z = p0 z * p0 w * p0 v + - p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z.
rewrite the current goal using add_CSNo_assoc (p0 z * p0 w * p0 v) (- p0 z * p1 v ' * p1 w) (- p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z) ?? ?? ?? (from right to left).
Use f_equal.
We will prove p0 z * (p0 w * p0 v + - p1 v ' * p1 w) = p0 z * p0 w * p0 v + - p0 z * p1 v ' * p1 w.
rewrite the current goal using mul_CSNo_distrL (p0 z) (p0 w * p0 v) (- p1 v ' * p1 w) ?? ?? ?? (from left to right).
We will prove p0 z * p0 w * p0 v + p0 z * (- p1 v ' * p1 w) = p0 z * p0 w * p0 v + - p0 z * p1 v ' * p1 w.
Use f_equal.
We will prove p0 z * (- p1 v ' * p1 w) = - p0 z * p1 v ' * p1 w.
An exact proof term for the current goal is minus_mul_CSNo_distrR (p0 z) (p1 v ' * p1 w) ?? ??.
We will prove - (p1 v * p0 w + p1 w * p0 v ') ' * p1 z = - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z.
Use transitivity with and - (p0 w ' * p1 v ' * p1 z + p0 v * p1 w ' * p1 z).
Use f_equal.
We will prove (p1 v * p0 w + p1 w * p0 v ') ' * p1 z = p0 w ' * p1 v ' * p1 z + p0 v * p1 w ' * p1 z.
Use transitivity with and (p0 w ' * p1 v ' + p0 v * p1 w ') * p1 z.
Use f_equal.
We will prove (p1 v * p0 w + p1 w * p0 v ') ' = p0 w ' * p1 v ' + p0 v * p1 w '.
Use transitivity with and (p1 v * p0 w) ' + (p1 w * p0 v ') '.
An exact proof term for the current goal is conj_add_CSNo (p1 v * p0 w) (p1 w * p0 v ') ?? ??.
We will prove (p1 v * p0 w) ' + (p1 w * p0 v ') ' = p0 w ' * p1 v ' + p0 v * p1 w '.
Use f_equal.
An exact proof term for the current goal is conj_mul_CSNo (p1 v) (p0 w) ?? ??.
rewrite the current goal using conj_mul_CSNo (p1 w) (p0 v ') ?? ?? (from left to right).
We will prove p0 v ' ' * p1 w ' = p0 v * p1 w '.
Use f_equal.
An exact proof term for the current goal is conj_CSNo_invol (p0 v) ??.
We will prove (p0 w ' * p1 v ' + p0 v * p1 w ') * p1 z = p0 w ' * p1 v ' * p1 z + p0 v * p1 w ' * p1 z.
rewrite the current goal using mul_CSNo_distrR (p0 w ' * p1 v ') (p0 v * p1 w ') (p1 z) ?? ?? ?? (from left to right).
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_CSNo_assoc (p0 w ') (p1 v ') (p1 z) ?? ?? ??.
Use symmetry.
An exact proof term for the current goal is mul_CSNo_assoc (p0 v) (p1 w ') (p1 z) ?? ?? ??.
We will prove - (p0 w ' * p1 v ' * p1 z + p0 v * p1 w ' * p1 z) = - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z.
An exact proof term for the current goal is minus_add_CSNo (p0 w ' * p1 v ' * p1 z) (p0 v * p1 w ' * p1 z) ?? ??.
We will prove p0 z * p0 w * p0 v + - p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z = p0 z * p0 w * p0 v + - p1 w ' * p1 z * p0 v + - p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w '.
Use f_equal.
We will prove - p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z + - p0 v * p1 w ' * p1 z = - p1 w ' * p1 z * p0 v + - p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w '.
rewrite the current goal using add_CSNo_rotate_3_1 (- p0 z * p1 v ' * p1 w) (- p0 w ' * p1 v ' * p1 z) (- p0 v * p1 w ' * p1 z) ?? ?? ?? (from left to right).
We will prove - p0 v * p1 w ' * p1 z + - p0 z * p1 v ' * p1 w + - p0 w ' * p1 v ' * p1 z = - p1 w ' * p1 z * p0 v + - p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w '.
Use f_equal.
We will prove - p0 v * p1 w ' * p1 z = - p1 w ' * p1 z * p0 v.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_CSNo_rotate_3_1 (p1 w ') (p1 z) (p0 v) ?? ?? ??.
Use f_equal.
We will prove - p0 z * p1 v ' * p1 w = - p1 v ' * p1 w * p0 z.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_CSNo_rotate_3_1 (p1 v ') (p1 w) (p0 z) ?? ?? ??.
We will prove - p0 w ' * p1 v ' * p1 z = - p1 v ' * p1 z * p0 w '.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_CSNo_rotate_3_1 (p1 v ') (p1 z) (p0 w ') ?? ?? ??.
We will prove p0 z * p0 w * p0 v + - p1 w ' * p1 z * p0 v + - p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w ' = (p0 z * p0 w + - p1 w ' * p1 z) * p0 v + - p1 v ' * (p1 w * p0 z + p1 z * p0 w ').
rewrite the current goal using add_CSNo_assoc (p0 z * p0 w * p0 v) (- p1 w ' * p1 z * p0 v) (- p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w ') ?? ?? ?? (from right to left).
Use f_equal.
We will prove p0 z * p0 w * p0 v + - p1 w ' * p1 z * p0 v = (p0 z * p0 w + - p1 w ' * p1 z) * p0 v.
rewrite the current goal using mul_CSNo_assoc (p0 z) (p0 w) (p0 v) ?? ?? ?? (from left to right).
We will prove (p0 z * p0 w) * p0 v + - p1 w ' * p1 z * p0 v = (p0 z * p0 w + - p1 w ' * p1 z) * p0 v.
rewrite the current goal using mul_CSNo_assoc (p1 w ') (p1 z) (p0 v) ?? ?? ?? (from left to right).
rewrite the current goal using minus_mul_CSNo_distrL (p1 w ' * p1 z) (p0 v) ?? ?? (from right to left).
We will prove (p0 z * p0 w) * p0 v + (- p1 w ' * p1 z) * p0 v = (p0 z * p0 w + - p1 w ' * p1 z) * p0 v.
Use symmetry.
An exact proof term for the current goal is mul_CSNo_distrR (p0 z * p0 w) (- p1 w ' * p1 z) (p0 v) ?? ?? ??.
We will prove - p1 v ' * p1 w * p0 z + - p1 v ' * p1 z * p0 w ' = - p1 v ' * (p1 w * p0 z + p1 z * p0 w ').
rewrite the current goal using minus_mul_CSNo_distrL (p1 v ') (p1 w * p0 z) ?? ?? (from right to left).
rewrite the current goal using minus_mul_CSNo_distrL (p1 v ') (p1 z * p0 w ') ?? ?? (from right to left).
rewrite the current goal using mul_CSNo_distrL (- p1 v ') (p1 w * p0 z) (p1 z * p0 w ') ?? ?? ?? (from right to left).
An exact proof term for the current goal is minus_mul_CSNo_distrL (p1 v ') (p1 w * p0 z + p1 z * p0 w ') ?? ??.
We will prove (p0 z * p0 w + - p1 w ' * p1 z) * p0 v + - p1 v ' * (p1 w * p0 z + p1 z * p0 w ') = p0 (mult' z w) * p0 v + - p1 v ' * p1 (mult' z w).
Use f_equal.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_HSNo_proj0 z w Hz Hw.
Use f_equal.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_HSNo_proj1 z w Hz Hw.
Use symmetry.
An exact proof term for the current goal is mul_HSNo_proj0 (mult' z w) v Lzw Hv.
We will prove p1 (mult' z (mult' w v)) = p1 (mult' (mult' z w) v).
Use transitivity with p1 (mult' w v) * p0 z + p1 z * p0 (mult' w v) ', (p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 w * p0 v + - (p1 v ' * p1 w)) ', (p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 v ' * p0 w ' + - p1 v * p1 w '), p1 v * p0 w * p0 z + p1 w * p0 v ' * p0 z + p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ', p1 v * p0 z * p0 w + - p1 v * p1 w ' * p1 z + p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ', p1 v * (p0 z * p0 w + - p1 w ' * p1 z) + (p1 w * p0 z + p1 z * p0 w ') * p0 v ', and p1 v * p0 (mult' z w) + p1 (mult' z w) * p0 v '.
An exact proof term for the current goal is mul_HSNo_proj1 z (mult' w v) Hz Lwv.
We will prove p1 (mult' w v) * p0 z + p1 z * p0 (mult' w v) ' = (p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 w * p0 v + - (p1 v ' * p1 w)) '.
Use f_equal.
Use f_equal.
An exact proof term for the current goal is mul_HSNo_proj1 w v Hw Hv.
Use f_equal.
Use f_equal.
An exact proof term for the current goal is mul_HSNo_proj0 w v Hw Hv.
We will prove (p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 w * p0 v + - (p1 v ' * p1 w)) ' = (p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 v ' * p0 w ' + - p1 v * p1 w ').
Use f_equal.
Use f_equal.
We will prove (p0 w * p0 v + - (p1 v ' * p1 w)) ' = p0 v ' * p0 w ' + - p1 v * p1 w '.
rewrite the current goal using conj_add_CSNo (p0 w * p0 v) (- (p1 v ' * p1 w)) ?? ?? (from left to right).
rewrite the current goal using conj_minus_CSNo (p1 v ' * p1 w) ?? (from left to right).
We will prove (p0 w * p0 v) ' + - (p1 v ' * p1 w) ' = p0 v ' * p0 w ' + - p1 v * p1 w '.
Use f_equal.
An exact proof term for the current goal is conj_mul_CSNo (p0 w) (p0 v) ?? ??.
Use f_equal.
rewrite the current goal using conj_mul_CSNo (p1 v ') (p1 w) ?? ?? (from left to right).
We will prove p1 w ' * p1 v ' ' = p1 v * p1 w '.
rewrite the current goal using conj_CSNo_invol (p1 v) ?? (from left to right).
We will prove p1 w ' * p1 v = p1 v * p1 w '.
An exact proof term for the current goal is mul_CSNo_com (p1 w ') (p1 v) ?? ??.
We will prove (p1 v * p0 w + p1 w * p0 v ') * p0 z + p1 z * (p0 v ' * p0 w ' + - p1 v * p1 w ') = p1 v * p0 w * p0 z + p1 w * p0 v ' * p0 z + p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w '.
rewrite the current goal using add_CSNo_assoc (p1 v * p0 w * p0 z) (p1 w * p0 v ' * p0 z) (p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ') ?? ?? ?? (from right to left).
Use f_equal.
We will prove (p1 v * p0 w + p1 w * p0 v ') * p0 z = p1 v * p0 w * p0 z + p1 w * p0 v ' * p0 z.
rewrite the current goal using mul_CSNo_distrR (p1 v * p0 w) (p1 w * p0 v ') (p0 z) ?? ?? ?? (from left to right).
rewrite the current goal using mul_CSNo_assoc (p1 v) (p0 w) (p0 z) ?? ?? ?? (from left to right).
rewrite the current goal using mul_CSNo_assoc (p1 w) (p0 v ') (p0 z) ?? ?? ?? (from left to right).
Use reflexivity.
We will prove p1 z * (p0 v ' * p0 w ' + - p1 v * p1 w ') = p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w '.
rewrite the current goal using mul_CSNo_distrL (p1 z) (p0 v ' * p0 w ') (- p1 v * p1 w ') ?? ?? ?? (from left to right).
Use f_equal.
We will prove p1 z * (- p1 v * p1 w ') = - p1 z * p1 v * p1 w '.
An exact proof term for the current goal is minus_mul_CSNo_distrR (p1 z) (p1 v * p1 w ') ?? ??.
We will prove p1 v * p0 w * p0 z + p1 w * p0 v ' * p0 z + p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ' = p1 v * p0 z * p0 w + - p1 v * p1 w ' * p1 z + p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v '.
Use f_equal.
Use f_equal.
An exact proof term for the current goal is mul_CSNo_com (p0 w) (p0 z) ?? ??.
We will prove p1 w * p0 v ' * p0 z + p1 z * p0 v ' * p0 w ' + - p1 z * p1 v * p1 w ' = - p1 v * p1 w ' * p1 z + p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v '.
rewrite the current goal using add_CSNo_rotate_3_1 (p1 w * p0 v ' * p0 z) (p1 z * p0 v ' * p0 w ') (- p1 z * p1 v * p1 w ') ?? ?? ?? (from left to right).
Use f_equal.
We will prove - p1 z * p1 v * p1 w ' = - p1 v * p1 w ' * p1 z.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_CSNo_rotate_3_1 (p1 v) (p1 w ') (p1 z) ?? ?? ??.
Use f_equal.
We will prove p1 w * p0 v ' * p0 z = p1 w * p0 z * p0 v '.
Use f_equal.
An exact proof term for the current goal is mul_CSNo_com (p0 v ') (p0 z) ?? ??.
We will prove p1 z * p0 v ' * p0 w ' = p1 z * p0 w ' * p0 v '.
Use f_equal.
An exact proof term for the current goal is mul_CSNo_com (p0 v ') (p0 w ') ?? ??.
We will prove p1 v * p0 z * p0 w + - p1 v * p1 w ' * p1 z + p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ' = p1 v * (p0 z * p0 w + - p1 w ' * p1 z) + (p1 w * p0 z + p1 z * p0 w ') * p0 v '.
rewrite the current goal using add_CSNo_assoc (p1 v * p0 z * p0 w) (- p1 v * p1 w ' * p1 z) (p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ') ?? ?? ?? (from right to left).
Use f_equal.
We will prove p1 v * p0 z * p0 w + - p1 v * p1 w ' * p1 z = p1 v * (p0 z * p0 w + - p1 w ' * p1 z).
rewrite the current goal using mul_CSNo_distrL (p1 v) (p0 z * p0 w) (- p1 w ' * p1 z) ?? ?? ?? (from left to right).
We will prove p1 v * p0 z * p0 w + - p1 v * p1 w ' * p1 z = p1 v * p0 z * p0 w + p1 v * (- p1 w ' * p1 z).
Use f_equal.
We will prove - p1 v * p1 w ' * p1 z = p1 v * (- p1 w ' * p1 z).
Use symmetry.
An exact proof term for the current goal is minus_mul_CSNo_distrR (p1 v) (p1 w ' * p1 z) ?? ??.
We will prove p1 w * p0 z * p0 v ' + p1 z * p0 w ' * p0 v ' = (p1 w * p0 z + p1 z * p0 w ') * p0 v '.
rewrite the current goal using mul_CSNo_assoc (p1 w) (p0 z) (p0 v ') ?? ?? ?? (from left to right).
rewrite the current goal using mul_CSNo_assoc (p1 z) (p0 w ') (p0 v ') ?? ?? ?? (from left to right).
Use symmetry.
An exact proof term for the current goal is mul_CSNo_distrR (p1 w * p0 z) (p1 z * p0 w ') (p0 v ') ?? ?? ??.
We will prove p1 v * (p0 z * p0 w + - p1 w ' * p1 z) + (p1 w * p0 z + p1 z * p0 w ') * p0 v ' = p1 v * p0 (mult' z w) + p1 (mult' z w) * p0 v '.
Use f_equal.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_HSNo_proj0 z w Hz Hw.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is mul_HSNo_proj1 z w Hz Hw.
Use symmetry.
We will prove p1 (mult' (mult' z w) v) = p1 v * p0 (mult' z w) + p1 (mult' z w) * p0 v '.
An exact proof term for the current goal is mul_HSNo_proj1 (mult' z w) v Lzw Hv.
∎
Theorem. (conj_HSNo_i)
i '' = :-: i
In Proofgold the corresponding term root is 04e5d9... and proposition id is f2cf1e...
Proof:
rewrite the current goal using conj_HSNo_conj_CSNo i CSNo_Complex_i (from left to right).
rewrite the current goal using minus_HSNo_minus_CSNo i CSNo_Complex_i (from left to right).
We will prove i ' = - i.
An exact proof term for the current goal is conj_CSNo_i.
∎
Theorem. (conj_HSNo_j)
j '' = :-: j
In Proofgold the corresponding term root is 6cfb40... and proposition id is b0aea8...
Proof:
Apply HSNo_proj0proj1_split (j '') (:-: j) (HSNo_conj_HSNo j HSNo_Quaternion_j) (HSNo_minus_HSNo j HSNo_Quaternion_j) to the current goal.
We will prove p0 (j '') = p0 (:-: j).
rewrite the current goal using conj_HSNo_proj0 j HSNo_Quaternion_j (from left to right).
rewrite the current goal using minus_HSNo_proj0 j HSNo_Quaternion_j (from left to right).
We will prove p0 j ' = - p0 j.
rewrite the current goal using HSNo_p0_j (from left to right).
We will prove 0 ' = - 0.
rewrite the current goal using minus_CSNo_0 (from left to right).
An exact proof term for the current goal is conj_CSNo_id_SNo 0 SNo_0.
We will prove p1 (j '') = p1 (:-: j).
rewrite the current goal using conj_HSNo_proj1 j HSNo_Quaternion_j (from left to right).
rewrite the current goal using minus_HSNo_proj1 j HSNo_Quaternion_j (from left to right).
We will prove - p1 j = - p1 j.
Use reflexivity.
∎
Theorem. (conj_HSNo_k)
k '' = :-: k
In Proofgold the corresponding term root is dfb947... and proposition id is 1f19c7...
Proof:
Apply HSNo_proj0proj1_split (k '') (:-: k) (HSNo_conj_HSNo k HSNo_Quaternion_k) (HSNo_minus_HSNo k HSNo_Quaternion_k) to the current goal.
We will prove p0 (k '') = p0 (:-: k).
rewrite the current goal using conj_HSNo_proj0 k HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_HSNo_proj0 k HSNo_Quaternion_k (from left to right).
We will prove p0 k ' = - p0 k.
rewrite the current goal using HSNo_p0_k (from left to right).
We will prove 0 ' = - 0.
rewrite the current goal using minus_CSNo_0 (from left to right).
An exact proof term for the current goal is conj_CSNo_id_SNo 0 SNo_0.
We will prove p1 (k '') = p1 (:-: k).
rewrite the current goal using conj_HSNo_proj1 k HSNo_Quaternion_k (from left to right).
rewrite the current goal using minus_HSNo_proj1 k HSNo_Quaternion_k (from left to right).
We will prove - p1 k = - p1 k.
Use reflexivity.
∎
End of Section SurQuaternions
Beginning of Section Quaternions
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_HSNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_HSNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_HSNo.
Let i ≝ Complex_i
Let j ≝ Quaternion_j
Let k ≝ Quaternion_k
Let p0 : set → set ≝ HSNo_proj0
Let p1 : set → set ≝ HSNo_proj1
Let pa : set → set → set ≝ CSNo_pair
Definition. We define quaternion to be {pa (u 0) (u 1)|u ∈ complex ⨯ complex} of type set.
In Proofgold the corresponding term root is dfa313... and object id is d9a819...
Theorem. (quaternion_I)
∀x y ∈ complex, pa x y ∈ quaternion
In Proofgold the corresponding term root is 5f5747... and proposition id is afcd2e...
Proof:
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
We will prove pa x y ∈ quaternion.
rewrite the current goal using tuple_2_0_eq x y (from right to left).
rewrite the current goal using tuple_2_1_eq x y (from right to left) at position 2.
We will prove pa ((x,y) 0) ((x,y) 1) ∈ quaternion.
Apply ReplI (complex ⨯ complex) (λu ⇒ pa (u 0) (u 1)) to the current goal.
We will prove (x,y) ∈ complex ⨯ complex.
An exact proof term for the current goal is tuple_2_setprod complex complex x Hx y Hy.
∎
Theorem. (quaternion_E)
∀z ∈ quaternion, ∀p : prop, (∀x y ∈ complex, z = pa x y → p) → p
In Proofgold the corresponding term root is 6a5a42... and proposition id is f4d94d...
Proof:
Let z be given.
Assume Hz.
Let p be given.
Assume Hp.
Apply ReplE_impred (complex ⨯ complex) (λu ⇒ pa (u 0) (u 1)) z Hz to the current goal.
Let u be given.
Assume Hu: u ∈ complex ⨯ complex.
Assume Hzu: z = pa (u 0) (u 1).
An exact proof term for the current goal is Hp (u 0) (ap0_Sigma complex (λ_ ⇒ complex) u Hu) (u 1) (ap1_Sigma complex (λ_ ⇒ complex) u Hu) Hzu.
∎
Theorem. (quaternion_HSNo)
∀z ∈ quaternion, HSNo z
In Proofgold the corresponding term root is 076f3c... and proposition id is 0af764...
Proof:
Let z be given.
Assume Hz.
Apply quaternion_E z Hz to the current goal.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Assume Hzxy: z = pa x y.
We will prove HSNo z.
rewrite the current goal using Hzxy (from left to right).
Apply HSNo_I to the current goal.
An exact proof term for the current goal is complex_CSNo x Hx.
An exact proof term for the current goal is complex_CSNo y Hy.
∎
Theorem. (complex_quaternion)
complex ⊆ quaternion
In Proofgold the corresponding term root is a6a6d6... and proposition id is da2811...
Proof:
Let x be given.
Assume Hx: x ∈ complex.
We will prove x ∈ quaternion.
rewrite the current goal using CSNo_pair_0 x (from right to left).
We will prove pa x 0 ∈ quaternion.
Apply quaternion_I to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is complex_0.
∎
Theorem. (quaternion_0)
0 ∈ quaternion
In Proofgold the corresponding term root is e063de... and proposition id is ff7551...
Proof:
An exact proof term for the current goal is complex_quaternion 0 complex_0.
∎
Theorem. (quaternion_1)
1 ∈ quaternion
In Proofgold the corresponding term root is 82d4bb... and proposition id is f8553f...
Proof:
An exact proof term for the current goal is complex_quaternion 1 complex_1.
∎
Theorem. (quaternion_i)
i ∈ quaternion
In Proofgold the corresponding term root is 2065ce... and proposition id is 885152...
Proof:
An exact proof term for the current goal is complex_quaternion i complex_i.
∎
Theorem. (quaternion_j)
j ∈ quaternion
In Proofgold the corresponding term root is 66ccff... and proposition id is 539f92...
Proof:
We will prove pa 0 1 ∈ quaternion.
Apply quaternion_I to the current goal.
An exact proof term for the current goal is complex_0.
An exact proof term for the current goal is complex_1.
∎
Theorem. (quaternion_k)
k ∈ quaternion
In Proofgold the corresponding term root is 8d9436... and proposition id is 57d22f...
Proof:
We will prove pa 0 i ∈ quaternion.
Apply quaternion_I to the current goal.
An exact proof term for the current goal is complex_0.
An exact proof term for the current goal is complex_i.
∎
Theorem. (quaternion_p0_eq)
∀x y ∈ complex, p0 (pa x y) = x
In Proofgold the corresponding term root is ffc962... and proposition id is be9c4d...
Proof:
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
An exact proof term for the current goal is HSNo_proj0_2 x y (complex_CSNo x Hx) (complex_CSNo y Hy).
∎
Theorem. (quaternion_p1_eq)
∀x y ∈ complex, p1 (pa x y) = y
In Proofgold the corresponding term root is f0d565... and proposition id is 24c854...
Proof:
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
An exact proof term for the current goal is HSNo_proj1_2 x y (complex_CSNo x Hx) (complex_CSNo y Hy).
∎
Theorem. (quaternion_p0_complex)
∀z ∈ quaternion, p0 z ∈ complex
In Proofgold the corresponding term root is a3df14... and proposition id is e1e097...
Proof:
Let z be given.
Assume Hz.
Apply quaternion_E z Hz to the current goal.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy Hzxy.
rewrite the current goal using Hzxy (from left to right).
We will prove p0 (pa x y) ∈ complex.
rewrite the current goal using quaternion_p0_eq x Hx y Hy (from left to right).
We will prove x ∈ complex.
An exact proof term for the current goal is Hx.
∎
Theorem. (quaternion_p1_complex)
∀z ∈ quaternion, p1 z ∈ complex
In Proofgold the corresponding term root is ac15b9... and proposition id is 32dd4d...
Proof:
Let z be given.
Assume Hz.
Apply quaternion_E z Hz to the current goal.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy Hzxy.
rewrite the current goal using Hzxy (from left to right).
We will prove p1 (pa x y) ∈ complex.
rewrite the current goal using quaternion_p1_eq x Hx y Hy (from left to right).
We will prove y ∈ complex.
An exact proof term for the current goal is Hy.
∎
Theorem. (quaternion_proj0proj1_split)
∀z w ∈ quaternion, p0 z = p0 w → p1 z = p1 w → z = w
In Proofgold the corresponding term root is 7d655c... and proposition id is 26e60b...
Proof:
Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
An exact proof term for the current goal is HSNo_proj0proj1_split z w (quaternion_HSNo z Hz) (quaternion_HSNo w Hw).
∎
Theorem. (quaternion_minus_HSNo)
∀z ∈ quaternion, - z ∈ quaternion
In Proofgold the corresponding term root is 8bff4e... and proposition id is df6a64...
Proof:
Let z be given.
Assume Hz.
We will prove pa (minus_CSNo (p0 z)) (minus_CSNo (p1 z)) ∈ quaternion.
Apply quaternion_I to the current goal.
Apply complex_minus_CSNo to the current goal.
An exact proof term for the current goal is quaternion_p0_complex z Hz.
Apply complex_minus_CSNo to the current goal.
An exact proof term for the current goal is quaternion_p1_complex z Hz.
∎
Theorem. (quaternion_conj_HSNo)
∀z ∈ quaternion, conj_HSNo z ∈ quaternion
In Proofgold the corresponding term root is ef83a8... and proposition id is 51db63...
Proof:
Let z be given.
Assume Hz.
We will prove pa (conj_CSNo (p0 z)) (minus_CSNo (p1 z)) ∈ quaternion.
Apply quaternion_I to the current goal.
Apply complex_conj_CSNo to the current goal.
An exact proof term for the current goal is quaternion_p0_complex z Hz.
Apply complex_minus_CSNo to the current goal.
An exact proof term for the current goal is quaternion_p1_complex z Hz.
∎
Theorem. (quaternion_add_HSNo)
∀z w ∈ quaternion, z + w ∈ quaternion
In Proofgold the corresponding term root is 2c4b19... and proposition id is 93e3ed...
Proof:
Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
We will prove pa (add_CSNo (p0 z) (p0 w)) (add_CSNo (p1 z) (p1 w)) ∈ quaternion.
Apply quaternion_I to the current goal.
Apply complex_add_CSNo to the current goal.
An exact proof term for the current goal is quaternion_p0_complex z Hz.
An exact proof term for the current goal is quaternion_p0_complex w Hw.
Apply complex_add_CSNo to the current goal.
An exact proof term for the current goal is quaternion_p1_complex z Hz.
An exact proof term for the current goal is quaternion_p1_complex w Hw.
∎
Theorem. (quaternion_mul_HSNo)
∀z w ∈ quaternion, z * w ∈ quaternion
In Proofgold the corresponding term root is c05871... and proposition id is f8fd5d...
Proof:
Let z be given.
Assume Hz.
Let w be given.
Assume Hw.
We will prove pa (add_CSNo (mul_CSNo (p0 z) (p0 w)) (minus_CSNo (mul_CSNo (conj_CSNo (p1 w)) (p1 z)))) (add_CSNo (mul_CSNo (p1 w) (p0 z)) (mul_CSNo (p1 z) (conj_CSNo (p0 w)))) ∈ quaternion.
We prove the intermediate claim Lz0: p0 z ∈ complex.
An exact proof term for the current goal is quaternion_p0_complex z Hz.
We prove the intermediate claim Lz1: p1 z ∈ complex.
An exact proof term for the current goal is quaternion_p1_complex z Hz.
We prove the intermediate claim Lw0: p0 w ∈ complex.
An exact proof term for the current goal is quaternion_p0_complex w Hw.
We prove the intermediate claim Lw1: p1 w ∈ complex.
An exact proof term for the current goal is quaternion_p1_complex w Hw.
Apply quaternion_I to the current goal.
Apply complex_add_CSNo to the current goal.
Apply complex_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply complex_minus_CSNo to the current goal.
Apply complex_mul_CSNo to the current goal.
Apply complex_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply complex_add_CSNo to the current goal.
Apply complex_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
Apply complex_mul_CSNo to the current goal.
An exact proof term for the current goal is ??.
Apply complex_conj_CSNo to the current goal.
An exact proof term for the current goal is ??.
∎
Theorem. (complex_p0_eq)
∀x ∈ complex, p0 x = x
In Proofgold the corresponding term root is 6a7777... and proposition id is 3e2e1f...
Proof:
Let x be given.
Assume Hx.
rewrite the current goal using CSNo_pair_0 x (from right to left) at position 1.
An exact proof term for the current goal is quaternion_p0_eq x Hx 0 complex_0.
∎
Theorem. (complex_p1_eq)
∀x ∈ complex, p1 x = 0
In Proofgold the corresponding term root is 498737... and proposition id is d0861d...
Proof:
Let x be given.
Assume Hx.
rewrite the current goal using CSNo_pair_0 x (from right to left).
An exact proof term for the current goal is quaternion_p1_eq x Hx 0 complex_0.
∎
End of Section Quaternions