Beginning of Section SurrealDiv
Notation. We use - as a prefix operator with priority 358 corresponding to applying term minus_SNo.
Notation. We use + as an infix operator with priority 360 and which associates to the right corresponding to applying term add_SNo.
Notation. We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term mul_SNo.
Notation. We use < as an infix operator with priority 490 and no associativity corresponding to applying term SNoLt.
Notation. We use ≤ as an infix operator with priority 490 and no associativity corresponding to applying term SNoLe.
Notation. We use ^ as an infix operator with priority 342 and which associates to the right corresponding to applying term exp_SNo_nat.
Definition. We define SNoL_pos to be λx ⇒ {w ∈ SNoL x|0 < w} of type set → set.
In Proofgold the corresponding term root is 399f06... and object id is 65d5ad...
Theorem. (SNo_recip_pos_pos)
∀x xi, SNo x → SNo xi → 0 < x → x * xi = 1 → 0 < xi
In Proofgold the corresponding term root is 8f0063... and proposition id is 5b48db...
Proof:
Let x and xi be given.
Assume Hx Hxi Hxpos Hxxi.
Apply SNoLt_trichotomy_or_impred 0 xi SNo_0 Hxi to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1: 0 = xi.
We will prove False.
Apply neq_0_1 to the current goal.
We will prove 0 = 1.
rewrite the current goal using Hxxi (from right to left).
We will prove 0 = x * xi.
rewrite the current goal using H1 (from right to left).
We will prove 0 = x * 0.
Use symmetry.
An exact proof term for the current goal is mul_SNo_zeroR x Hx.
Assume H1: xi < 0.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
Apply SNoLt_tra 0 1 0 SNo_0 SNo_1 SNo_0 SNoLt_0_1 to the current goal.
We will prove 1 < 0.
rewrite the current goal using Hxxi (from right to left).
We will prove x * xi < 0.
An exact proof term for the current goal is mul_SNo_pos_neg x xi Hx Hxi Hxpos H1.
∎
Theorem. (SNo_recip_lem1)
∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoL_pos x → SNo x'i → x' * x'i = 1 → SNo y → x * y < 1 → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → 1 < x * y'
In Proofgold the corresponding term root is 761151... and proposition id is b197c8...
Proof:
Let x, x', x'i, y and y' be given.
Assume Hx Hxpos Hx' Hx'i Hx'x'i Hy Hxy1 Hy' Hy'y.
Apply SepE (SNoL x) (λw ⇒ 0 < w) x' Hx' to the current goal.
Assume Hx'L: x' ∈ SNoL x.
Assume Hx'pos: 0 < x'.
Apply SNoL_E x Hx x' Hx'L to the current goal.
Assume Hx'1: SNo x'.
Assume Hx'2: SNoLev x' ∈ SNoLev x.
Assume Hx'3: x' < x.
We prove the intermediate claim Lxy: SNo (x * y).
An exact proof term for the current goal is SNo_mul_SNo x y Hx Hy.
We prove the intermediate claim Lxy': SNo (x * y').
An exact proof term for the current goal is SNo_mul_SNo x y' Hx Hy'.
We prove the intermediate claim L1: 0 < 1 + - x * y.
Apply add_SNo_minus_Lt2b 1 (x * y) 0 SNo_1 Lxy SNo_0 to the current goal.
We will prove 0 + x * y < 1.
rewrite the current goal using add_SNo_0L (x * y) Lxy (from left to right).
We will prove x * y < 1.
An exact proof term for the current goal is Hxy1.
We prove the intermediate claim L2: (x' + - x) * x'i < 0.
Apply mul_SNo_neg_pos (x' + - x) x'i (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hx'i to the current goal.
We will prove x' + - x < 0.
Apply add_SNo_minus_Lt1b x' x 0 Hx'1 Hx SNo_0 to the current goal.
We will prove x' < 0 + x.
rewrite the current goal using add_SNo_0L x Hx (from left to right).
An exact proof term for the current goal is Hx'3.
We will prove 0 < x'i.
An exact proof term for the current goal is SNo_recip_pos_pos x' x'i Hx'1 Hx'i Hx'pos Hx'x'i.
We prove the intermediate claim L3: 1 + - x * y' < 0.
rewrite the current goal using Hy'y (from left to right).
We will prove (1 + - x * y) * (x' + - x) * x'i < 0.
Apply mul_SNo_pos_neg (1 + - x * y) ((x' + - x) * x'i) (SNo_add_SNo 1 (- x * y) SNo_1 (SNo_minus_SNo (x * y) Lxy)) (SNo_mul_SNo (x' + - x) x'i (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hx'i) to the current goal.
An exact proof term for the current goal is L1.
An exact proof term for the current goal is L2.
We will prove 1 < x * y'.
rewrite the current goal using add_SNo_0L (x * y') Lxy' (from right to left).
We will prove 1 < 0 + x * y'.
An exact proof term for the current goal is add_SNo_minus_Lt1 1 (x * y') 0 SNo_1 Lxy' SNo_0 L3.
∎
Theorem. (SNo_recip_lem2)
∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoL_pos x → SNo x'i → x' * x'i = 1 → SNo y → 1 < x * y → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → x * y' < 1
In Proofgold the corresponding term root is 423150... and proposition id is 1a06f3...
Proof:
Let x, x', x'i, y and y' be given.
Assume Hx Hxpos Hx' Hx'i Hx'x'i Hy Hxy1 Hy' Hy'y.
Apply SepE (SNoL x) (λw ⇒ 0 < w) x' Hx' to the current goal.
Assume Hx'L: x' ∈ SNoL x.
Assume Hx'pos: 0 < x'.
Apply SNoL_E x Hx x' Hx'L to the current goal.
Assume Hx'1: SNo x'.
Assume Hx'2: SNoLev x' ∈ SNoLev x.
Assume Hx'3: x' < x.
We prove the intermediate claim Lxy: SNo (x * y).
An exact proof term for the current goal is SNo_mul_SNo x y Hx Hy.
We prove the intermediate claim Lxy': SNo (x * y').
An exact proof term for the current goal is SNo_mul_SNo x y' Hx Hy'.
We prove the intermediate claim L1: 1 + - x * y < 0.
Apply add_SNo_minus_Lt1b 1 (x * y) 0 SNo_1 Lxy SNo_0 to the current goal.
We will prove 1 < 0 + x * y.
rewrite the current goal using add_SNo_0L (x * y) Lxy (from left to right).
We will prove 1 < x * y.
An exact proof term for the current goal is Hxy1.
We prove the intermediate claim L2: (x' + - x) * x'i < 0.
Apply mul_SNo_neg_pos (x' + - x) x'i (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hx'i to the current goal.
We will prove x' + - x < 0.
Apply add_SNo_minus_Lt1b x' x 0 Hx'1 Hx SNo_0 to the current goal.
We will prove x' < 0 + x.
rewrite the current goal using add_SNo_0L x Hx (from left to right).
An exact proof term for the current goal is Hx'3.
We will prove 0 < x'i.
An exact proof term for the current goal is SNo_recip_pos_pos x' x'i Hx'1 Hx'i Hx'pos Hx'x'i.
We prove the intermediate claim L3: 0 < 1 + - x * y'.
rewrite the current goal using Hy'y (from left to right).
We will prove 0 < (1 + - x * y) * (x' + - x) * x'i.
Apply mul_SNo_neg_neg (1 + - x * y) ((x' + - x) * x'i) (SNo_add_SNo 1 (- x * y) SNo_1 (SNo_minus_SNo (x * y) Lxy)) (SNo_mul_SNo (x' + - x) x'i (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hx'i) to the current goal.
An exact proof term for the current goal is L1.
An exact proof term for the current goal is L2.
We will prove x * y' < 1.
rewrite the current goal using add_SNo_0L (x * y') Lxy' (from right to left).
We will prove 0 + x * y' < 1.
An exact proof term for the current goal is add_SNo_minus_Lt2 1 (x * y') 0 SNo_1 Lxy' SNo_0 L3.
∎
Theorem. (SNo_recip_lem3)
∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoR x → SNo x'i → x' * x'i = 1 → SNo y → x * y < 1 → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → x * y' < 1
In Proofgold the corresponding term root is b6e635... and proposition id is 22668c...
Proof:
Let x, x', x'i, y and y' be given.
Assume Hx Hxpos Hx' Hx'i Hx'x'i Hy Hxy1 Hy' Hy'y.
Apply SNoR_E x Hx x' Hx' to the current goal.
Assume Hx'1: SNo x'.
Assume Hx'2: SNoLev x' ∈ SNoLev x.
Assume Hx'3: x < x'.
We prove the intermediate claim Lxy: SNo (x * y).
An exact proof term for the current goal is SNo_mul_SNo x y Hx Hy.
We prove the intermediate claim Lxy': SNo (x * y').
An exact proof term for the current goal is SNo_mul_SNo x y' Hx Hy'.
We prove the intermediate claim Lx'pos: 0 < x'.
An exact proof term for the current goal is SNoLt_tra 0 x x' SNo_0 Hx Hx'1 Hxpos Hx'3.
We prove the intermediate claim L1: 0 < 1 + - x * y.
Apply add_SNo_minus_Lt2b 1 (x * y) 0 SNo_1 Lxy SNo_0 to the current goal.
We will prove 0 + x * y < 1.
rewrite the current goal using add_SNo_0L (x * y) Lxy (from left to right).
We will prove x * y < 1.
An exact proof term for the current goal is Hxy1.
We prove the intermediate claim L2: 0 < (x' + - x) * x'i.
Apply mul_SNo_pos_pos (x' + - x) x'i (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hx'i to the current goal.
We will prove 0 < x' + - x.
Apply add_SNo_minus_Lt2b x' x 0 Hx'1 Hx SNo_0 to the current goal.
We will prove 0 + x < x'.
rewrite the current goal using add_SNo_0L x Hx (from left to right).
An exact proof term for the current goal is Hx'3.
We will prove 0 < x'i.
An exact proof term for the current goal is SNo_recip_pos_pos x' x'i Hx'1 Hx'i Lx'pos Hx'x'i.
We prove the intermediate claim L3: 0 < 1 + - x * y'.
rewrite the current goal using Hy'y (from left to right).
We will prove 0 < (1 + - x * y) * (x' + - x) * x'i.
Apply mul_SNo_pos_pos (1 + - x * y) ((x' + - x) * x'i) (SNo_add_SNo 1 (- x * y) SNo_1 (SNo_minus_SNo (x * y) Lxy)) (SNo_mul_SNo (x' + - x) x'i (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hx'i) to the current goal.
An exact proof term for the current goal is L1.
An exact proof term for the current goal is L2.
We will prove x * y' < 1.
rewrite the current goal using add_SNo_0L (x * y') Lxy' (from right to left).
We will prove 0 + x * y' < 1.
An exact proof term for the current goal is add_SNo_minus_Lt2 1 (x * y') 0 SNo_1 Lxy' SNo_0 L3.
∎
Theorem. (SNo_recip_lem4)
∀x x' x'i y y', SNo x → 0 < x → x' ∈ SNoR x → SNo x'i → x' * x'i = 1 → SNo y → 1 < x * y → SNo y' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * x'i → 1 < x * y'
In Proofgold the corresponding term root is 417306... and proposition id is b572bc...
Proof:
Let x, x', x'i, y and y' be given.
Assume Hx Hxpos Hx' Hx'i Hx'x'i Hy Hxy1 Hy' Hy'y.
Apply SNoR_E x Hx x' Hx' to the current goal.
Assume Hx'1: SNo x'.
Assume Hx'2: SNoLev x' ∈ SNoLev x.
Assume Hx'3: x < x'.
We prove the intermediate claim Lxy: SNo (x * y).
An exact proof term for the current goal is SNo_mul_SNo x y Hx Hy.
We prove the intermediate claim Lxy': SNo (x * y').
An exact proof term for the current goal is SNo_mul_SNo x y' Hx Hy'.
We prove the intermediate claim Lx'pos: 0 < x'.
An exact proof term for the current goal is SNoLt_tra 0 x x' SNo_0 Hx Hx'1 Hxpos Hx'3.
We prove the intermediate claim L1: 1 + - x * y < 0.
Apply add_SNo_minus_Lt1b 1 (x * y) 0 SNo_1 Lxy SNo_0 to the current goal.
We will prove 1 < 0 + x * y.
rewrite the current goal using add_SNo_0L (x * y) Lxy (from left to right).
We will prove 1 < x * y.
An exact proof term for the current goal is Hxy1.
We prove the intermediate claim L2: 0 < (x' + - x) * x'i.
Apply mul_SNo_pos_pos (x' + - x) x'i (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hx'i to the current goal.
We will prove 0 < x' + - x.
Apply add_SNo_minus_Lt2b x' x 0 Hx'1 Hx SNo_0 to the current goal.
We will prove 0 + x < x'.
rewrite the current goal using add_SNo_0L x Hx (from left to right).
An exact proof term for the current goal is Hx'3.
We will prove 0 < x'i.
An exact proof term for the current goal is SNo_recip_pos_pos x' x'i Hx'1 Hx'i Lx'pos Hx'x'i.
We prove the intermediate claim L3: 1 + - x * y' < 0.
rewrite the current goal using Hy'y (from left to right).
We will prove (1 + - x * y) * (x' + - x) * x'i < 0.
Apply mul_SNo_neg_pos (1 + - x * y) ((x' + - x) * x'i) (SNo_add_SNo 1 (- x * y) SNo_1 (SNo_minus_SNo (x * y) Lxy)) (SNo_mul_SNo (x' + - x) x'i (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hx'i) to the current goal.
An exact proof term for the current goal is L1.
An exact proof term for the current goal is L2.
We will prove 1 < x * y'.
rewrite the current goal using add_SNo_0L (x * y') Lxy' (from right to left).
We will prove 1 < 0 + x * y'.
An exact proof term for the current goal is add_SNo_minus_Lt1 1 (x * y') 0 SNo_1 Lxy' SNo_0 L3.
∎
Definition. We define SNo_recipauxset to be λY x X g ⇒ ⋃y ∈ Y{(1 + (x' + - x) * y) * g x'|x' ∈ X} of type set → set → set → (set → set) → set.
In Proofgold the corresponding term root is f6355f... and object id is d40943...
Theorem. (SNo_recipauxset_I)
∀Y x X, ∀g : set → set, ∀y ∈ Y, ∀x' ∈ X, (1 + (x' + - x) * y) * g x' ∈ SNo_recipauxset Y x X g
In Proofgold the corresponding term root is fb23ea... and proposition id is 3cd34a...
Proof:
Let Y, x, X, g and y be given.
Assume Hy.
Let x' be given.
Assume Hx'.
We will prove (1 + (x' + - x) * y) * g x' ∈ ⋃y ∈ Y{(1 + (x' + - x) * y) * g x'|x' ∈ X}.
Apply famunionI Y (λy ⇒ {(1 + (x' + - x) * y) * g x'|x' ∈ X}) y ((1 + (x' + - x) * y) * g x') Hy to the current goal.
We will prove (1 + (x' + - x) * y) * g x' ∈ {(1 + (x' + - x) * y) * g x'|x' ∈ X}.
An exact proof term for the current goal is ReplI X (λx' ⇒ (1 + (x' + - x) * y) * g x') x' Hx'.
∎
Theorem. (SNo_recipauxset_E)
∀Y x X, ∀g : set → set, ∀z ∈ SNo_recipauxset Y x X g, ∀p : prop, (∀y ∈ Y, ∀x' ∈ X, z = (1 + (x' + - x) * y) * g x' → p) → p
In Proofgold the corresponding term root is ea0c30... and proposition id is 9c174a...
Proof:
Let Y, x, X, g and z be given.
Assume Hz.
Let p be given.
Assume H1.
Apply famunionE_impred Y (λy ⇒ {(1 + (x' + - x) * y) * g x'|x' ∈ X}) z Hz to the current goal.
Let y be given.
Assume Hy.
Assume H2: z ∈ {(1 + (x' + - x) * y) * g x'|x' ∈ X}.
Apply ReplE_impred X (λx' ⇒ (1 + (x' + - x) * y) * g x') z H2 to the current goal.
Let x' be given.
Assume Hx': x' ∈ X.
Assume H3: z = (1 + (x' + - x) * y) * g x'.
An exact proof term for the current goal is H1 y Hy x' Hx' H3.
∎
Theorem. (SNo_recipauxset_ext)
∀Y x X, ∀g h : set → set, (∀x' ∈ X, g x' = h x') → SNo_recipauxset Y x X g = SNo_recipauxset Y x X h
In Proofgold the corresponding term root is 7eb20f... and proposition id is a033a6...
Proof:
Let Y, x, X, g and h be given.
Assume Hgh.
We will prove (⋃y ∈ Y{(1 + (x' + - x) * y) * g x'|x' ∈ X}) = (⋃y ∈ Y{(1 + (x' + - x) * y) * h x'|x' ∈ X}).
Apply famunion_ext to the current goal.
Let y be given.
Assume Hy.
Apply ReplEq_ext X (λx' ⇒ (1 + (x' + - x) * y) * g x') (λx' ⇒ (1 + (x' + - x) * y) * h x') to the current goal.
Let x' be given.
Assume Hx'.
We will prove (1 + (x' + - x) * y) * g x' = (1 + (x' + - x) * y) * h x'.
Use f_equal.
An exact proof term for the current goal is Hgh x' Hx'.
∎
Definition. We define SNo_recipaux to be λx g ⇒ nat_primrec ({0},0) (λk p ⇒ (p 0 ∪ SNo_recipauxset (p 0) x (SNoR x) g ∪ SNo_recipauxset (p 1) x (SNoL_pos x) g,p 1 ∪ SNo_recipauxset (p 0) x (SNoL_pos x) g ∪ SNo_recipauxset (p 1) x (SNoR x) g)) of type set → (set → set) → set → set.
In Proofgold the corresponding term root is 8cdbea... and object id is 6fc28a...
Theorem. (SNo_recipaux_0)
∀x, ∀g : set → set, SNo_recipaux x g 0 = ({0},0)
In Proofgold the corresponding term root is 1a1104... and proposition id is a9fc4d...
Proof:
Let x and g be given.
An exact proof term for the current goal is nat_primrec_0 ({0},0) (λk p ⇒ (p 0 ∪ SNo_recipauxset (p 0) x (SNoR x) g ∪ SNo_recipauxset (p 1) x (SNoL_pos x) g,p 1 ∪ SNo_recipauxset (p 0) x (SNoL_pos x) g ∪ SNo_recipauxset (p 1) x (SNoR x) g)).
∎
Theorem. (SNo_recipaux_S)
∀x, ∀g : set → set, ∀n, nat_p n → SNo_recipaux x g (ordsucc n) = (SNo_recipaux x g n 0 ∪ SNo_recipauxset (SNo_recipaux x g n 0) x (SNoR x) g ∪ SNo_recipauxset (SNo_recipaux x g n 1) x (SNoL_pos x) g,SNo_recipaux x g n 1 ∪ SNo_recipauxset (SNo_recipaux x g n 0) x (SNoL_pos x) g ∪ SNo_recipauxset (SNo_recipaux x g n 1) x (SNoR x) g)
In Proofgold the corresponding term root is 35af7d... and proposition id is 55b106...
Proof:
Let x, g and n be given.
Assume Hn.
An exact proof term for the current goal is nat_primrec_S ({0},0) (λk p ⇒ (p 0 ∪ SNo_recipauxset (p 0) x (SNoR x) g ∪ SNo_recipauxset (p 1) x (SNoL_pos x) g,p 1 ∪ SNo_recipauxset (p 0) x (SNoL_pos x) g ∪ SNo_recipauxset (p 1) x (SNoR x) g)) n Hn.
∎
Theorem. (SNo_recipaux_lem1)
∀x, SNo x → 0 < x → ∀g : set → set, (∀x' ∈ SNoS_ (SNoLev x), 0 < x' → SNo (g x') ∧ x' * g x' = 1) → ∀k, nat_p k → (∀y ∈ SNo_recipaux x g k 0, SNo y ∧ x * y < 1) ∧ (∀y ∈ SNo_recipaux x g k 1, SNo y ∧ 1 < x * y)
In Proofgold the corresponding term root is af615d... and proposition id is 7c3309...
Proof:
Let x be given.
Assume Hx Hxpos.
Let g be given.
Assume Hg.
Set r to be the term SNo_recipaux x g.
We prove the intermediate claim L1: ∀x' ∈ SNoS_ (SNoLev x), 0 < x' → ∀y y', SNo y → y' = (1 + (x' + - x) * y) * g x' → SNo y'.
Let x' be given.
Assume Hx' Hx'pos.
Let y and y' be given.
Assume Hy Hy'.
Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) x' Hx' to the current goal.
Assume _ _ Hx'1 _.
rewrite the current goal using Hy' (from left to right).
Apply SNo_mul_SNo to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is SNo_1.
Apply SNo_mul_SNo to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx'1.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hy.
Apply Hg x' Hx' Hx'pos to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate claim L2: ∀x' ∈ SNoS_ (SNoLev x), 0 < x' → ∀y y', SNo y → y' = (1 + (x' + - x) * y) * g x' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * g x'.
Let x' be given.
Assume Hx' Hx'pos.
Let y and y' be given.
Assume Hy Hy'.
Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) x' Hx' to the current goal.
Assume _ _ Hx'1 _.
We will prove 1 + - x * y' = (1 + - x * y) * (x' + - x) * g x'.
Apply Hg x' Hx' Hx'pos to the current goal.
Assume Hgx'1 Hgx'2.
rewrite the current goal using mul_SNo_distrR x' (- x) (g x') Hx'1 (SNo_minus_SNo x Hx) Hgx'1 (from left to right).
We will prove 1 + - x * y' = (1 + - x * y) * (x' * g x' + (- x) * g x').
rewrite the current goal using Hgx'2 (from left to right).
We will prove 1 + - x * y' = (1 + - x * y) * (1 + (- x) * g x').
rewrite the current goal using SNo_foil 1 (- x * y) 1 ((- x) * g x') SNo_1 (SNo_minus_SNo (x * y) (SNo_mul_SNo x y Hx Hy)) SNo_1 (SNo_mul_SNo (- x) (g x') (SNo_minus_SNo x Hx) Hgx'1) (from left to right).
We will prove 1 + - x * y' = 1 * 1 + 1 * (- x) * g x' + (- x * y) * 1 + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_oneL 1 SNo_1 (from left to right).
rewrite the current goal using mul_SNo_oneL ((- x) * g x') (SNo_mul_SNo (- x) (g x') (SNo_minus_SNo x Hx) Hgx'1) (from left to right).
rewrite the current goal using mul_SNo_oneR (- x * y) (SNo_minus_SNo (x * y) (SNo_mul_SNo x y Hx Hy)) (from left to right).
We will prove 1 + - x * y' = 1 + (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
Use f_equal.
We will prove - x * y' = (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using Hy' (from left to right).
We will prove - x * ((1 + (x' + - x) * y) * g x') = (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_distrR 1 ((x' + - x) * y) (g x') SNo_1 (SNo_mul_SNo (x' + - x) y (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hy) Hgx'1 (from left to right).
We will prove - x * (1 * g x' + ((x' + - x) * y) * g x') = (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_oneL (g x') Hgx'1 (from left to right).
We will prove - x * (g x' + ((x' + - x) * y) * g x') = (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_minus_distrL x (g x' + ((x' + - x) * y) * g x') Hx (SNo_add_SNo (g x') (((x' + - x) * y) * g x') Hgx'1 (SNo_mul_SNo ((x' + - x) * y) (g x') (SNo_mul_SNo (x' + - x) y (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hy) Hgx'1)) (from right to left).
We will prove (- x) * (g x' + ((x' + - x) * y) * g x') = (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_distrL (- x) (g x') (((x' + - x) * y) * g x') (SNo_minus_SNo x Hx) Hgx'1 (SNo_mul_SNo ((x' + - x) * y) (g x') (SNo_mul_SNo (x' + - x) y (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hy) Hgx'1) (from left to right).
We will prove (- x) * g x' + (- x) * (((x' + - x) * y) * g x') = (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
Use f_equal.
We will prove (- x) * (((x' + - x) * y) * g x') = - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_distrR x' (- x) y Hx'1 (SNo_minus_SNo x Hx) Hy (from left to right).
We will prove (- x) * ((x' * y + (- x) * y) * g x') = - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_distrR (x' * y) ((- x) * y) (g x') (SNo_mul_SNo x' y Hx'1 Hy) (SNo_mul_SNo (- x) y (SNo_minus_SNo x Hx) Hy) Hgx'1 (from left to right).
We will prove (- x) * ((x' * y) * g x' + ((- x) * y) * g x') = - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_com x' y Hx'1 Hy (from left to right).
rewrite the current goal using mul_SNo_assoc y x' (g x') Hy Hx'1 Hgx'1 (from right to left).
rewrite the current goal using Hgx'2 (from left to right).
rewrite the current goal using mul_SNo_oneR y Hy (from left to right).
We will prove (- x) * (y + ((- x) * y) * g x') = - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_distrL (- x) y (((- x) * y) * g x') (SNo_minus_SNo x Hx) Hy (SNo_mul_SNo ((- x) * y) (g x') (SNo_mul_SNo (- x) y (SNo_minus_SNo x Hx) Hy) Hgx'1) (from left to right).
We will prove (- x) * y + (- x) * ((- x) * y) * g x' = - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_minus_distrL x y Hx Hy (from left to right) at position 1.
We will prove - x * y + (- x) * ((- x) * y) * g x' = - x * y + (- x * y) * (- x) * g x'.
Use f_equal.
We will prove (- x) * ((- x) * y) * g x' = (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_assoc (- x) ((- x) * y) (g x') (SNo_minus_SNo x Hx) (SNo_mul_SNo (- x) y (SNo_minus_SNo x Hx) Hy) Hgx'1 (from left to right).
rewrite the current goal using mul_SNo_assoc (- x * y) (- x) (g x') (SNo_minus_SNo (x * y) (SNo_mul_SNo x y Hx Hy)) (SNo_minus_SNo x Hx) Hgx'1 (from left to right).
Use f_equal.
We will prove (- x) * ((- x) * y) = (- x * y) * (- x).
rewrite the current goal using mul_SNo_com (- x) y (SNo_minus_SNo x Hx) Hy (from left to right).
We will prove (- x) * (y * (- x)) = (- x * y) * (- x).
rewrite the current goal using mul_SNo_minus_distrL x y Hx Hy (from right to left).
We will prove (- x) * (y * (- x)) = ((- x) * y) * (- x).
An exact proof term for the current goal is mul_SNo_assoc (- x) y (- x) (SNo_minus_SNo x Hx) Hy (SNo_minus_SNo x Hx).
Apply nat_ind to the current goal.
Apply andI to the current goal.
Let y be given.
We will prove y ∈ r 0 0 → SNo y ∧ x * y < 1.
rewrite the current goal using SNo_recipaux_0 (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
We will prove y ∈ {0} → SNo y ∧ x * y < 1.
Assume H1: y ∈ {0}.
rewrite the current goal using SingE 0 y H1 (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is SNo_0.
We will prove x * 0 < 1.
rewrite the current goal using mul_SNo_zeroR x Hx (from left to right).
An exact proof term for the current goal is SNoLt_0_1.
Let y be given.
We will prove y ∈ r 0 1 → SNo y ∧ 1 < x * y.
rewrite the current goal using SNo_recipaux_0 (from left to right).
We will prove y ∈ ({0},0) 1 → SNo y ∧ 1 < x * y.
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove y ∈ 0 → SNo y ∧ 1 < x * y.
Assume H1: y ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE y H1.
Let k be given.
Assume Hk: nat_p k.
Assume IH.
Apply IH to the current goal.
Assume IH1: ∀y ∈ r k 0, SNo y ∧ x * y < 1.
Assume IH2: ∀y ∈ r k 1, SNo y ∧ 1 < x * y.
Apply andI to the current goal.
Let y' be given.
We will prove y' ∈ r (ordsucc k) 0 → SNo y' ∧ x * y' < 1.
rewrite the current goal using SNo_recipaux_S (from left to right).
We will prove y' ∈ (r k 0 ∪ SNo_recipauxset (r k 0) x (SNoR x) g ∪ SNo_recipauxset (r k 1) x (SNoL_pos x) g,r k 1 ∪ SNo_recipauxset (r k 0) x (SNoL_pos x) g ∪ SNo_recipauxset (r k 1) x (SNoR x) g) 0 → SNo y' ∧ x * y' < 1.
rewrite the current goal using tuple_2_0_eq (from left to right).
We will prove y' ∈ r k 0 ∪ SNo_recipauxset (r k 0) x (SNoR x) g ∪ SNo_recipauxset (r k 1) x (SNoL_pos x) g → SNo y' ∧ x * y' < 1.
Assume H1.
Apply binunionE (r k 0 ∪ SNo_recipauxset (r k 0) x (SNoR x) g) (SNo_recipauxset (r k 1) x (SNoL_pos x) g) y' H1 to the current goal.
Assume H1.
Apply binunionE (r k 0) (SNo_recipauxset (r k 0) x (SNoR x) g) y' H1 to the current goal.
An exact proof term for the current goal is IH1 y'.
Assume H1.
Apply SNo_recipauxset_E (r k 0) x (SNoR x) g y' H1 to the current goal.
Let y be given.
Assume Hy: y ∈ r k 0.
Let x' be given.
Assume Hx': x' ∈ SNoR x.
Assume H2: y' = (1 + (x' + - x) * y) * g x'.
Apply SNoR_E x Hx x' Hx' to the current goal.
Assume Hx'1 Hx'2 Hx'3.
We prove the intermediate claim Lx': x' ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 x' x Hx'1 Hx Hx'2 to the current goal.
We prove the intermediate claim Lx'pos: 0 < x'.
An exact proof term for the current goal is SNoLt_tra 0 x x' SNo_0 Hx Hx'1 Hxpos Hx'3.
Apply IH1 y Hy to the current goal.
Assume Hy1: SNo y.
Assume Hxy1: x * y < 1.
Apply Hg x' Lx' Lx'pos to the current goal.
Assume Hgx'1: SNo (g x').
Assume Hgx'2: x' * g x' = 1.
We prove the intermediate claim Ly': SNo y'.
An exact proof term for the current goal is L1 x' Lx' Lx'pos y y' Hy1 H2.
Apply andI to the current goal.
An exact proof term for the current goal is Ly'.
Apply SNo_recip_lem3 x x' (g x') y y' Hx Hxpos Hx' Hgx'1 Hgx'2 Hy1 Hxy1 Ly' to the current goal.
We will prove 1 + - x * y' = (1 + - x * y) * (x' + - x) * g x'.
An exact proof term for the current goal is L2 x' Lx' Lx'pos y y' Hy1 H2.
Assume H1.
Apply SNo_recipauxset_E (r k 1) x (SNoL_pos x) g y' H1 to the current goal.
Let y be given.
Assume Hy: y ∈ r k 1.
Let x' be given.
Assume Hx': x' ∈ SNoL_pos x.
Assume H2: y' = (1 + (x' + - x) * y) * g x'.
Apply SepE (SNoL x) (λw ⇒ 0 < w) x' Hx' to the current goal.
Assume Hx'0: x' ∈ SNoL x.
Assume Hx'pos: 0 < x'.
Apply SNoL_E x Hx x' Hx'0 to the current goal.
Assume Hx'1 Hx'2 Hx'3.
We prove the intermediate claim Lx': x' ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 x' x Hx'1 Hx Hx'2 to the current goal.
Apply IH2 y Hy to the current goal.
Assume Hy1: SNo y.
Assume Hxy1: 1 < x * y.
Apply Hg x' Lx' Hx'pos to the current goal.
Assume Hgx'1: SNo (g x').
Assume Hgx'2: x' * g x' = 1.
We prove the intermediate claim Ly': SNo y'.
An exact proof term for the current goal is L1 x' Lx' Hx'pos y y' Hy1 H2.
Apply andI to the current goal.
An exact proof term for the current goal is Ly'.
Apply SNo_recip_lem2 x x' (g x') y y' Hx Hxpos Hx' Hgx'1 Hgx'2 Hy1 Hxy1 Ly' to the current goal.
We will prove 1 + - x * y' = (1 + - x * y) * (x' + - x) * g x'.
An exact proof term for the current goal is L2 x' Lx' Hx'pos y y' Hy1 H2.
An exact proof term for the current goal is Hk.
Let y' be given.
We will prove y' ∈ r (ordsucc k) 1 → SNo y' ∧ 1 < x * y'.
rewrite the current goal using SNo_recipaux_S (from left to right).
We will prove y' ∈ (r k 0 ∪ SNo_recipauxset (r k 0) x (SNoR x) g ∪ SNo_recipauxset (r k 1) x (SNoL_pos x) g,r k 1 ∪ SNo_recipauxset (r k 0) x (SNoL_pos x) g ∪ SNo_recipauxset (r k 1) x (SNoR x) g) 1 → SNo y' ∧ 1 < x * y'.
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove y' ∈ r k 1 ∪ SNo_recipauxset (r k 0) x (SNoL_pos x) g ∪ SNo_recipauxset (r k 1) x (SNoR x) g → SNo y' ∧ 1 < x * y'.
Assume H1.
Apply binunionE (r k 1 ∪ SNo_recipauxset (r k 0) x (SNoL_pos x) g) (SNo_recipauxset (r k 1) x (SNoR x) g) y' H1 to the current goal.
Assume H1.
Apply binunionE (r k 1) (SNo_recipauxset (r k 0) x (SNoL_pos x) g) y' H1 to the current goal.
An exact proof term for the current goal is IH2 y'.
Assume H1.
Apply SNo_recipauxset_E (r k 0) x (SNoL_pos x) g y' H1 to the current goal.
Let y be given.
Assume Hy: y ∈ r k 0.
Let x' be given.
Assume Hx': x' ∈ SNoL_pos x.
Assume H2: y' = (1 + (x' + - x) * y) * g x'.
Apply SepE (SNoL x) (λw ⇒ 0 < w) x' Hx' to the current goal.
Assume Hx'0: x' ∈ SNoL x.
Assume Hx'pos: 0 < x'.
Apply SNoL_E x Hx x' Hx'0 to the current goal.
Assume Hx'1 Hx'2 Hx'3.
We prove the intermediate claim Lx': x' ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 x' x Hx'1 Hx Hx'2 to the current goal.
Apply IH1 y Hy to the current goal.
Assume Hy1: SNo y.
Assume Hxy1: x * y < 1.
Apply Hg x' Lx' Hx'pos to the current goal.
Assume Hgx'1: SNo (g x').
Assume Hgx'2: x' * g x' = 1.
We prove the intermediate claim Ly': SNo y'.
An exact proof term for the current goal is L1 x' Lx' Hx'pos y y' Hy1 H2.
Apply andI to the current goal.
An exact proof term for the current goal is Ly'.
Apply SNo_recip_lem1 x x' (g x') y y' Hx Hxpos Hx' Hgx'1 Hgx'2 Hy1 Hxy1 Ly' to the current goal.
We will prove 1 + - x * y' = (1 + - x * y) * (x' + - x) * g x'.
An exact proof term for the current goal is L2 x' Lx' Hx'pos y y' Hy1 H2.
Assume H1.
Apply SNo_recipauxset_E (r k 1) x (SNoR x) g y' H1 to the current goal.
Let y be given.
Assume Hy: y ∈ r k 1.
Let x' be given.
Assume Hx': x' ∈ SNoR x.
Assume H2: y' = (1 + (x' + - x) * y) * g x'.
Apply SNoR_E x Hx x' Hx' to the current goal.
Assume Hx'1 Hx'2 Hx'3.
We prove the intermediate claim Lx': x' ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 x' x Hx'1 Hx Hx'2 to the current goal.
We prove the intermediate claim Lx'pos: 0 < x'.
An exact proof term for the current goal is SNoLt_tra 0 x x' SNo_0 Hx Hx'1 Hxpos Hx'3.
Apply IH2 y Hy to the current goal.
Assume Hy1: SNo y.
Assume Hxy1: 1 < x * y.
Apply Hg x' Lx' Lx'pos to the current goal.
Assume Hgx'1: SNo (g x').
Assume Hgx'2: x' * g x' = 1.
We prove the intermediate claim Ly': SNo y'.
An exact proof term for the current goal is L1 x' Lx' Lx'pos y y' Hy1 H2.
Apply andI to the current goal.
An exact proof term for the current goal is Ly'.
Apply SNo_recip_lem4 x x' (g x') y y' Hx Hxpos Hx' Hgx'1 Hgx'2 Hy1 Hxy1 Ly' to the current goal.
We will prove 1 + - x * y' = (1 + - x * y) * (x' + - x) * g x'.
An exact proof term for the current goal is L2 x' Lx' Lx'pos y y' Hy1 H2.
An exact proof term for the current goal is Hk.
∎
Theorem. (SNo_recipaux_lem2)
∀x, SNo x → 0 < x → ∀g : set → set, (∀x' ∈ SNoS_ (SNoLev x), 0 < x' → SNo (g x') ∧ x' * g x' = 1) → SNoCutP (⋃k ∈ ωSNo_recipaux x g k 0) (⋃k ∈ ωSNo_recipaux x g k 1)
In Proofgold the corresponding term root is 38996c... and proposition id is c6f6db...
Proof:
Let x be given.
Assume Hx Hxpos.
Let g be given.
Assume Hg.
Set L to be the term ⋃k ∈ ωSNo_recipaux x g k 0.
Set R to be the term ⋃k ∈ ωSNo_recipaux x g k 1.
We will prove (∀x ∈ L, SNo x) ∧ (∀y ∈ R, SNo y) ∧ (∀x ∈ L, ∀y ∈ R, x < y).
We prove the intermediate claim L1: ∀k, nat_p k → (∀y ∈ SNo_recipaux x g k 0, SNo y ∧ x * y < 1) ∧ (∀y ∈ SNo_recipaux x g k 1, SNo y ∧ 1 < x * y).
An exact proof term for the current goal is SNo_recipaux_lem1 x Hx Hxpos g Hg.
Apply and3I to the current goal.
Let y be given.
Assume Hy.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x g k 0) y Hy to the current goal.
Let k be given.
Assume Hk.
Assume H1: y ∈ SNo_recipaux x g k 0.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume H2 _.
Apply H2 y H1 to the current goal.
Assume H3 _.
An exact proof term for the current goal is H3.
Let y be given.
Assume Hy.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x g k 1) y Hy to the current goal.
Let k be given.
Assume Hk.
Assume H1: y ∈ SNo_recipaux x g k 1.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume _ H2.
Apply H2 y H1 to the current goal.
Assume H3 _.
An exact proof term for the current goal is H3.
Let w be given.
Assume Hw.
Let z be given.
Assume Hz.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x g k 0) w Hw to the current goal.
Let k be given.
Assume Hk.
Assume H1: w ∈ SNo_recipaux x g k 0.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume H2 _.
Apply H2 w H1 to the current goal.
Assume H3: SNo w.
Assume H4: x * w < 1.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x g k 1) z Hz to the current goal.
Let k' be given.
Assume Hk'.
Assume H5: z ∈ SNo_recipaux x g k' 1.
Apply L1 k' (omega_nat_p k' Hk') to the current goal.
Assume _ H6.
Apply H6 z H5 to the current goal.
Assume H7: SNo z.
Assume H8: 1 < x * z.
We will prove w < z.
Apply SNoLtLe_or w z H3 H7 to the current goal.
Assume H9: w < z.
An exact proof term for the current goal is H9.
Assume H9: z ≤ w.
We will prove False.
Apply SNoLt_irref 1 to the current goal.
We will prove 1 < 1.
Apply SNoLt_tra 1 (x * z) 1 SNo_1 (SNo_mul_SNo x z Hx H7) SNo_1 H8 to the current goal.
We will prove x * z < 1.
Apply SNoLeLt_tra (x * z) (x * w) 1 (SNo_mul_SNo x z Hx H7) (SNo_mul_SNo x w Hx H3) SNo_1 to the current goal.
We will prove x * z ≤ x * w.
Apply nonneg_mul_SNo_Le x z w Hx (SNoLtLe 0 x Hxpos) H7 H3 H9 to the current goal.
We will prove x * w < 1.
An exact proof term for the current goal is H4.
∎
Theorem. (SNo_recipaux_ext)
∀x, SNo x → ∀g h : set → set, (∀x' ∈ SNoS_ (SNoLev x), g x' = h x') → ∀k, nat_p k → SNo_recipaux x g k = SNo_recipaux x h k
In Proofgold the corresponding term root is b2de41... and proposition id is e7b024...
Proof:
Let x be given.
Assume Hx.
Let g and h be given.
Assume Hgh.
Apply nat_ind to the current goal.
We will prove SNo_recipaux x g 0 = SNo_recipaux x h 0.
rewrite the current goal using SNo_recipaux_0 x h (from left to right).
An exact proof term for the current goal is SNo_recipaux_0 x g.
Let k be given.
Assume Hk: nat_p k.
Assume IH: SNo_recipaux x g k = SNo_recipaux x h k.
We will prove SNo_recipaux x g (ordsucc k) = SNo_recipaux x h (ordsucc k).
rewrite the current goal using SNo_recipaux_S x g k Hk (from left to right).
rewrite the current goal using SNo_recipaux_S x h k Hk (from left to right).
We will prove (SNo_recipaux x g k 0 ∪ SNo_recipauxset (SNo_recipaux x g k 0) x (SNoR x) g ∪ SNo_recipauxset (SNo_recipaux x g k 1) x (SNoL_pos x) g,SNo_recipaux x g k 1 ∪ SNo_recipauxset (SNo_recipaux x g k 0) x (SNoL_pos x) g ∪ SNo_recipauxset (SNo_recipaux x g k 1) x (SNoR x) g) = (SNo_recipaux x h k 0 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) h ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) h,SNo_recipaux x h k 1 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) h ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) h).
rewrite the current goal using IH (from left to right).
We will prove (SNo_recipaux x h k 0 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) g ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) g,SNo_recipaux x h k 1 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) g ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) g) = (SNo_recipaux x h k 0 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) h ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) h,SNo_recipaux x h k 1 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) h ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) h).
We prove the intermediate claim L1: SNo_recipaux x h k 0 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) g ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) g = SNo_recipaux x h k 0 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) h ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) h.
Use f_equal.
Use f_equal.
We will prove SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) g = SNo_recipauxset (SNo_recipaux x h k 0) x (SNoR x) h.
Apply SNo_recipauxset_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
We will prove g w = h w.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
We will prove SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) g = SNo_recipauxset (SNo_recipaux x h k 1) x (SNoL_pos x) h.
Apply SNo_recipauxset_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL_pos x.
We will prove g w = h w.
Apply SNoL_E x Hx w (SepE1 (SNoL x) (λw ⇒ 0 < w) w Hw) to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
We prove the intermediate claim L2: SNo_recipaux x h k 1 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) g ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) g = SNo_recipaux x h k 1 ∪ SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) h ∪ SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) h.
Use f_equal.
Use f_equal.
We will prove SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) g = SNo_recipauxset (SNo_recipaux x h k 0) x (SNoL_pos x) h.
Apply SNo_recipauxset_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL_pos x.
We will prove g w = h w.
Apply SNoL_E x Hx w (SepE1 (SNoL x) (λw ⇒ 0 < w) w Hw) to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
We will prove SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) g = SNo_recipauxset (SNo_recipaux x h k 1) x (SNoR x) h.
Apply SNo_recipauxset_ext to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
We will prove g w = h w.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
We will prove w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
rewrite the current goal using L1 (from left to right).
rewrite the current goal using L2 (from left to right).
Use reflexivity.
∎
Beginning of Section recip_SNo_pos
Let G : set → (set → set) → set ≝ λx g ⇒ SNoCut (⋃k ∈ ωSNo_recipaux x g k 0) (⋃k ∈ ωSNo_recipaux x g k 1)
Definition. We define recip_SNo_pos to be SNo_rec_i G of type set → set.
In Proofgold the corresponding term root is 88641a... and object id is 2f4ee1...
Theorem. (recip_SNo_pos_eq)
∀x, SNo x → recip_SNo_pos x = G x recip_SNo_pos
In Proofgold the corresponding term root is 2e3e0e... and proposition id is ebab77...
Proof:
Apply SNo_rec_i_eq G to the current goal.
Let x be given.
Assume Hx.
Let g and h be given.
Assume Hgh.
We will prove SNoCut (⋃k ∈ ωSNo_recipaux x g k 0) (⋃k ∈ ωSNo_recipaux x g k 1) = SNoCut (⋃k ∈ ωSNo_recipaux x h k 0) (⋃k ∈ ωSNo_recipaux x h k 1).
Use f_equal.
Apply famunion_ext to the current goal.
Let k be given.
Assume Hk.
We will prove SNo_recipaux x g k 0 = SNo_recipaux x h k 0.
Use f_equal.
Apply SNo_recipaux_ext x Hx g h to the current goal.
We will prove ∀w ∈ SNoS_ (SNoLev x), g w = h w.
An exact proof term for the current goal is Hgh.
An exact proof term for the current goal is omega_nat_p k Hk.
Apply famunion_ext to the current goal.
Let k be given.
Assume Hk.
We will prove SNo_recipaux x g k 1 = SNo_recipaux x h k 1.
Use f_equal.
Apply SNo_recipaux_ext x Hx g h to the current goal.
We will prove ∀w ∈ SNoS_ (SNoLev x), g w = h w.
An exact proof term for the current goal is Hgh.
An exact proof term for the current goal is omega_nat_p k Hk.
∎
Theorem. (recip_SNo_pos_prop1)
∀x, SNo x → 0 < x → SNo (recip_SNo_pos x) ∧ x * recip_SNo_pos x = 1
In Proofgold the corresponding term root is 42138c... and proposition id is 785262...
Proof:
Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx: SNo x.
Assume IH: ∀w ∈ SNoS_ (SNoLev x), 0 < w → SNo (recip_SNo_pos w) ∧ w * recip_SNo_pos w = 1.
Assume Hxpos: 0 < x.
We will prove SNo (recip_SNo_pos x) ∧ x * recip_SNo_pos x = 1.
rewrite the current goal using recip_SNo_pos_eq x Hx (from left to right).
We will prove SNo (G x recip_SNo_pos) ∧ x * G x recip_SNo_pos = 1.
Set L to be the term ⋃k ∈ ωSNo_recipaux x recip_SNo_pos k 0.
Set R to be the term ⋃k ∈ ωSNo_recipaux x recip_SNo_pos k 1.
We prove the intermediate claim L1: ∀k, nat_p k → (∀y ∈ SNo_recipaux x recip_SNo_pos k 0, SNo y ∧ x * y < 1) ∧ (∀y ∈ SNo_recipaux x recip_SNo_pos k 1, SNo y ∧ 1 < x * y).
An exact proof term for the current goal is SNo_recipaux_lem1 x Hx Hxpos recip_SNo_pos IH.
We prove the intermediate claim L1L: ∀w ∈ L, x * w < 1.
Let w be given.
Assume Hw.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) w Hw to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: w ∈ SNo_recipaux x recip_SNo_pos k 0.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume H2 _.
Apply H2 w H1 to the current goal.
Assume _ H3.
An exact proof term for the current goal is H3.
We prove the intermediate claim L1R: ∀z ∈ R, 1 < x * z.
Let z be given.
Assume Hz.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 1) z Hz to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: z ∈ SNo_recipaux x recip_SNo_pos k 1.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume _ H2.
Apply H2 z H1 to the current goal.
Assume _ H3.
An exact proof term for the current goal is H3.
We prove the intermediate claim L2: SNoCutP L R.
An exact proof term for the current goal is SNo_recipaux_lem2 x Hx Hxpos recip_SNo_pos IH.
Apply L2 to the current goal.
Assume HLHR.
Apply HLHR to the current goal.
Assume HL: ∀w ∈ L, SNo w.
Assume HR: ∀z ∈ R, SNo z.
Assume HLR: ∀w ∈ L, ∀z ∈ R, w < z.
Set y to be the term SNoCut L R.
Apply SNoCutP_SNoCut_impred L R L2 to the current goal.
Assume H1: SNo y.
Assume H2: SNoLev y ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Assume H3: ∀w ∈ L, w < y.
Assume H4: ∀z ∈ R, y < z.
Assume H5: ∀u, SNo u → (∀w ∈ L, w < u) → (∀z ∈ R, u < z) → SNoLev y ⊆ SNoLev u ∧ SNoEq_ (SNoLev y) y u.
We prove the intermediate claim L3: SNo (x * y).
An exact proof term for the current goal is SNo_mul_SNo x y Hx H1.
We prove the intermediate claim L4: 0 < y.
Apply H3 to the current goal.
We will prove 0 ∈ L.
Apply famunionI ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) 0 to the current goal.
We will prove 0 ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_0.
We will prove 0 ∈ SNo_recipaux x recip_SNo_pos 0 0.
rewrite the current goal using SNo_recipaux_0 (from left to right).
We will prove 0 ∈ ({0},0) 0.
rewrite the current goal using tuple_2_0_eq (from left to right).
Apply SingI to the current goal.
We prove the intermediate claim L5: 0 < x * y.
An exact proof term for the current goal is mul_SNo_pos_pos x y Hx H1 Hxpos L4.
We prove the intermediate claim L6: ∀w ∈ SNoL y, ∃w' ∈ L, w ≤ w'.
An exact proof term for the current goal is SNoL_SNoCutP_ex L R L2.
We prove the intermediate claim L7: ∀z ∈ SNoR y, ∃z' ∈ R, z' ≤ z.
An exact proof term for the current goal is SNoR_SNoCutP_ex L R L2.
Apply andI to the current goal.
We will prove SNo y.
An exact proof term for the current goal is H1.
We will prove x * y = 1.
Apply dneg to the current goal.
Assume HC: x * y ≠ 1.
Apply SNoLt_trichotomy_or_impred (x * y) 1 L3 SNo_1 to the current goal.
Assume H6: x * y < 1.
We prove the intermediate claim L8: 1 ∈ SNoR (x * y).
Apply SNoR_I to the current goal.
An exact proof term for the current goal is L3.
An exact proof term for the current goal is SNo_1.
We will prove SNoLev 1 ∈ SNoLev (x * y).
rewrite the current goal using ordinal_SNoLev 1 ordinal_1 (from left to right).
We will prove 1 ∈ SNoLev (x * y).
Apply ordinal_In_Or_Subq 1 (SNoLev (x * y)) ordinal_1 (SNoLev_ordinal (x * y) L3) to the current goal.
Assume H7: 1 ∈ SNoLev (x * y).
An exact proof term for the current goal is H7.
Assume H7: SNoLev (x * y) ⊆ 1.
We will prove False.
Apply HC to the current goal.
We will prove x * y = 1.
An exact proof term for the current goal is pos_low_eq_one (x * y) L3 L5 H7.
An exact proof term for the current goal is H6.
We prove the intermediate claim L9: ∀v w w', SNo v → SNo w → SNo w' → v ∈ SNoS_ (SNoLev x) → 0 < v → v * y + x * w ≤ 1 + v * w → (1 + (v + - x) * w') * recip_SNo_pos v ∈ L → (- v + x) * w' ≤ (- v + x) * w → False.
Let v, w and w' be given.
Assume Hv1 Hw1 Hw' HvS Hvpos H7 Hw'' H8.
Set w'' to be the term (1 + (v + - x) * w') * recip_SNo_pos v.
We prove the intermediate claim Lw''1: SNo w''.
An exact proof term for the current goal is HL w'' Hw''.
Apply SNoLt_irref 1 to the current goal.
We will prove 1 < 1.
Apply SNoLtLe_tra 1 (1 + v * (y + - w'')) 1 SNo_1 (SNo_add_SNo 1 (v * (y + - w'')) SNo_1 (SNo_mul_SNo v (y + - w'') Hv1 (SNo_add_SNo y (- w'') H1 (SNo_minus_SNo w'' Lw''1)))) SNo_1 to the current goal.
We will prove 1 < 1 + v * (y + - w'').
rewrite the current goal using add_SNo_0R 1 SNo_1 (from right to left) at position 1.
We will prove 1 + 0 < 1 + v * (y + - w'').
Apply add_SNo_Lt2 1 0 (v * (y + - w'')) SNo_1 SNo_0 (SNo_mul_SNo v (y + - w'') Hv1 (SNo_add_SNo y (- w'') H1 (SNo_minus_SNo w'' Lw''1))) to the current goal.
We will prove 0 < v * (y + - w'').
Apply mul_SNo_pos_pos v (y + - w'') Hv1 (SNo_add_SNo y (- w'') H1 (SNo_minus_SNo w'' Lw''1)) Hvpos to the current goal.
We will prove 0 < y + - w''.
Apply SNoLt_minus_pos w'' y Lw''1 H1 to the current goal.
We will prove w'' < y.
An exact proof term for the current goal is H3 w'' Hw''.
We will prove 1 + v * (y + - w'') ≤ 1.
rewrite the current goal using mul_SNo_distrL v y (- w'') Hv1 H1 (SNo_minus_SNo w'' Lw''1) (from left to right).
We will prove 1 + v * y + v * (- w'') ≤ 1.
rewrite the current goal using mul_SNo_minus_distrR v w'' Hv1 Lw''1 (from left to right).
We will prove 1 + v * y + - v * w'' ≤ 1.
We will prove 1 + v * y + - v * (1 + (v + - x) * w') * recip_SNo_pos v ≤ 1.
Apply IH v HvS Hvpos to the current goal.
Assume Hrv1: SNo (recip_SNo_pos v).
Assume Hrv2: v * recip_SNo_pos v = 1.
rewrite the current goal using mul_SNo_com (1 + (v + - x) * w') (recip_SNo_pos v) (SNo_add_SNo 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) Hrv1 (from left to right).
We will prove 1 + v * y + - v * recip_SNo_pos v * (1 + (v + - x) * w') ≤ 1.
rewrite the current goal using mul_SNo_assoc v (recip_SNo_pos v) (1 + (v + - x) * w') Hv1 Hrv1 (SNo_add_SNo 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (from left to right).
We will prove 1 + v * y + - (v * recip_SNo_pos v) * (1 + (v + - x) * w') ≤ 1.
rewrite the current goal using Hrv2 (from left to right).
We will prove 1 + v * y + - 1 * (1 + (v + - x) * w') ≤ 1.
rewrite the current goal using mul_SNo_oneL (1 + (v + - x) * w') (SNo_add_SNo 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (from left to right).
We will prove 1 + v * y + - (1 + (v + - x) * w') ≤ 1.
rewrite the current goal using minus_add_SNo_distr 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw') (from left to right).
We will prove 1 + v * y + - 1 + - (v + - x) * w' ≤ 1.
rewrite the current goal using add_SNo_rotate_3_1 (- 1) (- (v + - x) * w') (v * y) (SNo_minus_SNo 1 SNo_1) (SNo_minus_SNo ((v + - x) * w') (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (SNo_mul_SNo v y Hv1 H1) (from right to left).
We will prove 1 + - 1 + - (v + - x) * w' + v * y ≤ 1.
rewrite the current goal using add_SNo_minus_SNo_prop2 1 (- (v + - x) * w' + v * y) SNo_1 (SNo_add_SNo (- (v + - x) * w') (v * y) (SNo_minus_SNo ((v + - x) * w') (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (SNo_mul_SNo v y Hv1 H1)) (from left to right).
We will prove - (v + - x) * w' + v * y ≤ 1.
rewrite the current goal using mul_SNo_minus_distrL (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw' (from right to left).
We will prove (- (v + - x)) * w' + v * y ≤ 1.
rewrite the current goal using minus_add_SNo_distr v (- x) Hv1 (SNo_minus_SNo x Hx) (from left to right).
rewrite the current goal using minus_SNo_invol x Hx (from left to right).
We will prove (- v + x) * w' + v * y ≤ 1.
Apply SNoLe_tra ((- v + x) * w' + v * y) ((- v + x) * w + v * y) 1 (SNo_add_SNo ((- v + x) * w') (v * y) (SNo_mul_SNo (- v + x) w' (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw') (SNo_mul_SNo v y Hv1 H1)) (SNo_add_SNo ((- v + x) * w) (v * y) (SNo_mul_SNo (- v + x) w (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw1) (SNo_mul_SNo v y Hv1 H1)) SNo_1 to the current goal.
We will prove (- v + x) * w' + v * y ≤ (- v + x) * w + v * y.
Apply add_SNo_Le1 ((- v + x) * w') (v * y) ((- v + x) * w) (SNo_mul_SNo (- v + x) w' (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw') (SNo_mul_SNo v y Hv1 H1) (SNo_mul_SNo (- v + x) w (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw1) to the current goal.
We will prove (- v + x) * w' ≤ (- v + x) * w.
An exact proof term for the current goal is H8.
We will prove (- v + x) * w + v * y ≤ 1.
rewrite the current goal using mul_SNo_distrR (- v) x w (SNo_minus_SNo v Hv1) Hx Hw1 (from left to right).
We will prove ((- v) * w + x * w) + v * y ≤ 1.
rewrite the current goal using mul_SNo_minus_distrL v w Hv1 Hw1 (from left to right).
We will prove (- v * w + x * w) + v * y ≤ 1.
rewrite the current goal using add_SNo_assoc (- v * w) (x * w) (v * y) (SNo_minus_SNo (v * w) (SNo_mul_SNo v w Hv1 Hw1)) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1) (from right to left).
We will prove - v * w + x * w + v * y ≤ 1.
rewrite the current goal using add_SNo_com (- v * w) (x * w + v * y) (SNo_minus_SNo (v * w) (SNo_mul_SNo v w Hv1 Hw1)) (SNo_add_SNo (x * w) (v * y) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1)) (from left to right).
Apply add_SNo_minus_Le2 1 (- v * w) (x * w + v * y) SNo_1 (SNo_minus_SNo (v * w) (SNo_mul_SNo v w Hv1 Hw1)) (SNo_add_SNo (x * w) (v * y) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1)) to the current goal.
We will prove x * w + v * y ≤ 1 + - - v * w.
rewrite the current goal using minus_SNo_invol (v * w) (SNo_mul_SNo v w Hv1 Hw1) (from left to right).
We will prove x * w + v * y ≤ 1 + v * w.
rewrite the current goal using add_SNo_com (x * w) (v * y) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1) (from left to right).
We will prove v * y + x * w ≤ 1 + v * w.
An exact proof term for the current goal is H7.
Apply mul_SNo_SNoR_interpolate_impred x y Hx H1 1 L8 to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL x.
Let w be given.
Assume Hw: w ∈ SNoR y.
Assume H7: v * y + x * w ≤ 1 + v * w.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: v < x.
Apply SNoR_E y H1 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: y < w.
We prove the intermediate claim LvS: v ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 v x Hv1 Hx Hv2.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
Apply L7 w Hw to the current goal.
Let w' be given.
Assume Hw'.
Apply Hw' to the current goal.
Assume Hw'1: w' ∈ R.
Assume Hw'2: w' ≤ w.
We prove the intermediate claim Lw': SNo w'.
An exact proof term for the current goal is HR w' Hw'1.
We prove the intermediate claim Lxw': SNo (x * w').
An exact proof term for the current goal is SNo_mul_SNo x w' Hx Lw'.
We prove the intermediate claim Lvpos: 0 < v.
Apply SNoLtLe_or 0 v SNo_0 Hv1 to the current goal.
Assume H8: 0 < v.
An exact proof term for the current goal is H8.
Assume H8: v ≤ 0.
We will prove False.
Apply SNoLt_irref 1 to the current goal.
We will prove 1 < 1.
Apply SNoLtLe_tra 1 (x * w') 1 SNo_1 Lxw' SNo_1 to the current goal.
We will prove 1 < x * w'.
An exact proof term for the current goal is L1R w' Hw'1.
We will prove x * w' ≤ 1.
Apply SNoLe_tra (x * w') (x * w) 1 Lxw' Lxw SNo_1 to the current goal.
We will prove x * w' ≤ x * w.
An exact proof term for the current goal is nonneg_mul_SNo_Le x w' w Hx (SNoLtLe 0 x Hxpos) Lw' Hw1 Hw'2.
We will prove x * w ≤ 1.
Apply SNoLe_tra (x * w) (v * (y + - w) + x * w) 1 Lxw (SNo_add_SNo (v * (y + - w)) (x * w) (SNo_mul_SNo v (y + - w) Hv1 (SNo_add_SNo y (- w) H1 (SNo_minus_SNo w Hw1))) Lxw) SNo_1 to the current goal.
We will prove x * w ≤ v * (y + - w) + x * w.
rewrite the current goal using add_SNo_0L (x * w) Lxw (from right to left) at position 1.
We will prove 0 + x * w ≤ v * (y + - w) + x * w.
Apply add_SNo_Le1 0 (x * w) (v * (y + - w)) SNo_0 Lxw (SNo_mul_SNo v (y + - w) Hv1 (SNo_add_SNo y (- w) H1 (SNo_minus_SNo w Hw1))) to the current goal.
We will prove 0 ≤ v * (y + - w).
Apply mul_SNo_nonpos_neg v (y + - w) Hv1 (SNo_add_SNo y (- w) H1 (SNo_minus_SNo w Hw1)) H8 to the current goal.
We will prove y + - w < 0.
Apply add_SNo_minus_Lt1b y w 0 H1 Hw1 SNo_0 to the current goal.
We will prove y < 0 + w.
rewrite the current goal using add_SNo_0L w Hw1 (from left to right).
We will prove y < w.
An exact proof term for the current goal is Hw3.
We will prove v * (y + - w) + x * w ≤ 1.
rewrite the current goal using mul_SNo_distrL v y (- w) Hv1 H1 (SNo_minus_SNo w Hw1) (from left to right).
We will prove (v * y + v * (- w)) + x * w ≤ 1.
rewrite the current goal using add_SNo_com_3b_1_2 (v * y) (v * (- w)) (x * w) (SNo_mul_SNo v y Hv1 H1) (SNo_mul_SNo v (- w) Hv1 (SNo_minus_SNo w Hw1)) Lxw (from left to right).
We will prove (v * y + x * w) + v * (- w) ≤ 1.
Apply add_SNo_minus_Le2 1 (v * (- w)) (v * y + x * w) SNo_1 (SNo_mul_SNo v (- w) Hv1 (SNo_minus_SNo w Hw1)) (SNo_add_SNo (v * y) (x * w) (SNo_mul_SNo v y Hv1 H1) Lxw) to the current goal.
We will prove v * y + x * w ≤ 1 + - v * (- w).
rewrite the current goal using mul_SNo_minus_distrR v w Hv1 Hw1 (from left to right).
rewrite the current goal using minus_SNo_invol (v * w) (SNo_mul_SNo v w Hv1 Hw1) (from left to right).
An exact proof term for the current goal is H7.
Set w'' to be the term (1 + (v + - x) * w') * recip_SNo_pos v.
We prove the intermediate claim Lw'': w'' ∈ L.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 1) w' Hw'1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H9: w' ∈ SNo_recipaux x recip_SNo_pos k 1.
Apply famunionI ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) (ordsucc k) w'' (omega_ordsucc k Hk) to the current goal.
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos (ordsucc k) 0.
rewrite the current goal using SNo_recipaux_S x recip_SNo_pos k (omega_nat_p k Hk) (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos k 0 ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoR x) recip_SNo_pos ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoL_pos x) recip_SNo_pos.
Apply binunionI2 to the current goal.
We will prove w'' ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoL_pos x) recip_SNo_pos.
Apply SNo_recipauxset_I (SNo_recipaux x recip_SNo_pos k 1) x (SNoL_pos x) recip_SNo_pos to the current goal.
We will prove w' ∈ SNo_recipaux x recip_SNo_pos k 1.
An exact proof term for the current goal is H9.
We will prove v ∈ SNoL_pos x.
We will prove v ∈ {w ∈ SNoL x|0 < w}.
Apply SepI to the current goal.
An exact proof term for the current goal is Hv.
We will prove 0 < v.
An exact proof term for the current goal is Lvpos.
Apply L9 v w w' Hv1 Hw1 Lw' LvS Lvpos H7 Lw'' to the current goal.
We will prove (- v + x) * w' ≤ (- v + x) * w.
Apply nonneg_mul_SNo_Le (- v + x) w' w (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) to the current goal.
We will prove 0 ≤ - v + x.
rewrite the current goal using add_SNo_com (- v) x (SNo_minus_SNo v Hv1) Hx (from left to right).
We will prove 0 ≤ x + - v.
Apply add_SNo_minus_Le2b x v 0 Hx Hv1 SNo_0 to the current goal.
We will prove 0 + v ≤ x.
rewrite the current goal using add_SNo_0L v Hv1 (from left to right).
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hv3.
An exact proof term for the current goal is Lw'.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is Hw'2.
Let v be given.
Assume Hv: v ∈ SNoR x.
Let w be given.
Assume Hw: w ∈ SNoL y.
Assume H7: v * y + x * w ≤ 1 + v * w.
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: x < v.
Apply SNoL_E y H1 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: w < y.
We prove the intermediate claim LvS: v ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 v x Hv1 Hx Hv2.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
Apply L6 w Hw to the current goal.
Let w' be given.
Assume Hw'.
Apply Hw' to the current goal.
Assume Hw'1: w' ∈ L.
Assume Hw'2: w ≤ w'.
We prove the intermediate claim Lw': SNo w'.
An exact proof term for the current goal is HL w' Hw'1.
We prove the intermediate claim Lxw': SNo (x * w').
An exact proof term for the current goal is SNo_mul_SNo x w' Hx Lw'.
We prove the intermediate claim Lvpos: 0 < v.
An exact proof term for the current goal is SNoLt_tra 0 x v SNo_0 Hx Hv1 Hxpos Hv3.
Set w'' to be the term (1 + (v + - x) * w') * recip_SNo_pos v.
We prove the intermediate claim Lw'': w'' ∈ L.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) w' Hw'1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H9: w' ∈ SNo_recipaux x recip_SNo_pos k 0.
Apply famunionI ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) (ordsucc k) w'' (omega_ordsucc k Hk) to the current goal.
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos (ordsucc k) 0.
rewrite the current goal using SNo_recipaux_S x recip_SNo_pos k (omega_nat_p k Hk) (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos k 0 ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoR x) recip_SNo_pos ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoL_pos x) recip_SNo_pos.
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
We will prove w'' ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoR x) recip_SNo_pos.
Apply SNo_recipauxset_I (SNo_recipaux x recip_SNo_pos k 0) x (SNoR x) recip_SNo_pos to the current goal.
We will prove w' ∈ SNo_recipaux x recip_SNo_pos k 0.
An exact proof term for the current goal is H9.
We will prove v ∈ SNoR x.
An exact proof term for the current goal is Hv.
Apply L9 v w w' Hv1 Hw1 Lw' LvS Lvpos H7 Lw'' to the current goal.
We will prove (- v + x) * w' ≤ (- v + x) * w.
Apply nonpos_mul_SNo_Le (- v + x) w' w (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) to the current goal.
We will prove - v + x ≤ 0.
rewrite the current goal using add_SNo_com (- v) x (SNo_minus_SNo v Hv1) Hx (from left to right).
We will prove x + - v ≤ 0.
Apply add_SNo_minus_Le2 0 (- v) x SNo_0 (SNo_minus_SNo v Hv1) Hx to the current goal.
rewrite the current goal using minus_SNo_invol v Hv1 (from left to right).
We will prove x ≤ 0 + v.
rewrite the current goal using add_SNo_0L v Hv1 (from left to right).
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hv3.
An exact proof term for the current goal is Lw'.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is Hw'2.
Assume H6: x * y = 1.
Apply HC to the current goal.
An exact proof term for the current goal is H6.
Assume H6: 1 < x * y.
We prove the intermediate claim L10: 1 ∈ SNoL (x * y).
Apply SNoL_I to the current goal.
An exact proof term for the current goal is L3.
An exact proof term for the current goal is SNo_1.
We will prove SNoLev 1 ∈ SNoLev (x * y).
rewrite the current goal using ordinal_SNoLev 1 ordinal_1 (from left to right).
We will prove 1 ∈ SNoLev (x * y).
Apply ordinal_In_Or_Subq 1 (SNoLev (x * y)) ordinal_1 (SNoLev_ordinal (x * y) L3) to the current goal.
Assume H7: 1 ∈ SNoLev (x * y).
An exact proof term for the current goal is H7.
Assume H7: SNoLev (x * y) ⊆ 1.
We will prove False.
Apply HC to the current goal.
We will prove x * y = 1.
An exact proof term for the current goal is pos_low_eq_one (x * y) L3 L5 H7.
An exact proof term for the current goal is H6.
We prove the intermediate claim L11: ∀v w w', SNo v → SNo w → SNo w' → v ∈ SNoS_ (SNoLev x) → 0 < v → 1 + v * w ≤ v * y + x * w → (1 + (v + - x) * w') * recip_SNo_pos v ∈ R → (- v + x) * w ≤ (- v + x) * w' → False.
Let v, w and w' be given.
Assume Hv1 Hw1 Hw' HvS Hvpos H7 Hw'' H8.
Set w'' to be the term (1 + (v + - x) * w') * recip_SNo_pos v.
We prove the intermediate claim Lw''1: SNo w''.
An exact proof term for the current goal is HR w'' Hw''.
Apply SNoLt_irref 1 to the current goal.
We will prove 1 < 1.
Apply SNoLeLt_tra 1 (1 + v * (y + - w'')) 1 SNo_1 (SNo_add_SNo 1 (v * (y + - w'')) SNo_1 (SNo_mul_SNo v (y + - w'') Hv1 (SNo_add_SNo y (- w'') H1 (SNo_minus_SNo w'' Lw''1)))) SNo_1 to the current goal.
We will prove 1 ≤ 1 + v * (y + - w'').
rewrite the current goal using mul_SNo_distrL v y (- w'') Hv1 H1 (SNo_minus_SNo w'' Lw''1) (from left to right).
We will prove 1 ≤ 1 + v * y + v * (- w'').
rewrite the current goal using mul_SNo_minus_distrR v w'' Hv1 Lw''1 (from left to right).
We will prove 1 ≤ 1 + v * y + - v * w''.
We will prove 1 ≤ 1 + v * y + - v * (1 + (v + - x) * w') * recip_SNo_pos v.
Apply IH v HvS Hvpos to the current goal.
Assume Hrv1: SNo (recip_SNo_pos v).
Assume Hrv2: v * recip_SNo_pos v = 1.
rewrite the current goal using mul_SNo_com (1 + (v + - x) * w') (recip_SNo_pos v) (SNo_add_SNo 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) Hrv1 (from left to right).
We will prove 1 ≤ 1 + v * y + - v * recip_SNo_pos v * (1 + (v + - x) * w').
rewrite the current goal using mul_SNo_assoc v (recip_SNo_pos v) (1 + (v + - x) * w') Hv1 Hrv1 (SNo_add_SNo 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (from left to right).
We will prove 1 ≤ 1 + v * y + - (v * recip_SNo_pos v) * (1 + (v + - x) * w').
rewrite the current goal using Hrv2 (from left to right).
We will prove 1 ≤ 1 + v * y + - 1 * (1 + (v + - x) * w').
rewrite the current goal using mul_SNo_oneL (1 + (v + - x) * w') (SNo_add_SNo 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (from left to right).
We will prove 1 ≤ 1 + v * y + - (1 + (v + - x) * w').
rewrite the current goal using minus_add_SNo_distr 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw') (from left to right).
We will prove 1 ≤ 1 + v * y + - 1 + - (v + - x) * w'.
rewrite the current goal using add_SNo_rotate_3_1 (- 1) (- (v + - x) * w') (v * y) (SNo_minus_SNo 1 SNo_1) (SNo_minus_SNo ((v + - x) * w') (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (SNo_mul_SNo v y Hv1 H1) (from right to left).
We will prove 1 ≤ 1 + - 1 + - (v + - x) * w' + v * y.
rewrite the current goal using add_SNo_minus_SNo_prop2 1 (- (v + - x) * w' + v * y) SNo_1 (SNo_add_SNo (- (v + - x) * w') (v * y) (SNo_minus_SNo ((v + - x) * w') (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (SNo_mul_SNo v y Hv1 H1)) (from left to right).
We will prove 1 ≤ - (v + - x) * w' + v * y.
rewrite the current goal using mul_SNo_minus_distrL (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw' (from right to left).
We will prove 1 ≤ (- (v + - x)) * w' + v * y.
rewrite the current goal using minus_add_SNo_distr v (- x) Hv1 (SNo_minus_SNo x Hx) (from left to right).
rewrite the current goal using minus_SNo_invol x Hx (from left to right).
We will prove 1 ≤ (- v + x) * w' + v * y.
Apply SNoLe_tra 1 ((- v + x) * w + v * y) ((- v + x) * w' + v * y) SNo_1 (SNo_add_SNo ((- v + x) * w) (v * y) (SNo_mul_SNo (- v + x) w (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw1) (SNo_mul_SNo v y Hv1 H1)) (SNo_add_SNo ((- v + x) * w') (v * y) (SNo_mul_SNo (- v + x) w' (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw') (SNo_mul_SNo v y Hv1 H1)) to the current goal.
We will prove 1 ≤ (- v + x) * w + v * y.
rewrite the current goal using mul_SNo_distrR (- v) x w (SNo_minus_SNo v Hv1) Hx Hw1 (from left to right).
We will prove 1 ≤ ((- v) * w + x * w) + v * y.
rewrite the current goal using mul_SNo_minus_distrL v w Hv1 Hw1 (from left to right).
We will prove 1 ≤ (- v * w + x * w) + v * y.
rewrite the current goal using add_SNo_assoc (- v * w) (x * w) (v * y) (SNo_minus_SNo (v * w) (SNo_mul_SNo v w Hv1 Hw1)) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1) (from right to left).
We will prove 1 ≤ - v * w + x * w + v * y.
rewrite the current goal using add_SNo_com (- v * w) (x * w + v * y) (SNo_minus_SNo (v * w) (SNo_mul_SNo v w Hv1 Hw1)) (SNo_add_SNo (x * w) (v * y) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1)) (from left to right).
We will prove 1 ≤ (x * w + v * y) + - v * w.
Apply add_SNo_minus_Le2b (x * w + v * y) (v * w) 1 (SNo_add_SNo (x * w) (v * y) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1)) (SNo_mul_SNo v w Hv1 Hw1) SNo_1 to the current goal.
We will prove 1 + v * w ≤ x * w + v * y.
rewrite the current goal using add_SNo_com (x * w) (v * y) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1) (from left to right).
We will prove 1 + v * w ≤ v * y + x * w.
An exact proof term for the current goal is H7.
We will prove (- v + x) * w + v * y ≤ (- v + x) * w' + v * y.
Apply add_SNo_Le1 ((- v + x) * w) (v * y) ((- v + x) * w') (SNo_mul_SNo (- v + x) w (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw1) (SNo_mul_SNo v y Hv1 H1) (SNo_mul_SNo (- v + x) w' (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw') to the current goal.
We will prove (- v + x) * w ≤ (- v + x) * w'.
An exact proof term for the current goal is H8.
We will prove 1 + v * (y + - w'') < 1.
rewrite the current goal using add_SNo_0R 1 SNo_1 (from right to left) at position 4.
We will prove 1 + v * (y + - w'') < 1 + 0.
Apply add_SNo_Lt2 1 (v * (y + - w'')) 0 SNo_1 (SNo_mul_SNo v (y + - w'') Hv1 (SNo_add_SNo y (- w'') H1 (SNo_minus_SNo w'' Lw''1))) SNo_0 to the current goal.
We will prove v * (y + - w'') < 0.
Apply mul_SNo_pos_neg v (y + - w'') Hv1 (SNo_add_SNo y (- w'') H1 (SNo_minus_SNo w'' Lw''1)) Hvpos to the current goal.
We will prove y + - w'' < 0.
Apply add_SNo_minus_Lt1b y w'' 0 H1 Lw''1 SNo_0 to the current goal.
We will prove y < 0 + w''.
rewrite the current goal using add_SNo_0L w'' Lw''1 (from left to right).
We will prove y < w''.
An exact proof term for the current goal is H4 w'' Hw''.
Apply mul_SNo_SNoL_interpolate_impred x y Hx H1 1 L10 to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL x.
Let w be given.
Assume Hw: w ∈ SNoL y.
Assume H7: 1 + v * w ≤ v * y + x * w.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: v < x.
Apply SNoL_E y H1 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: w < y.
We prove the intermediate claim LvS: v ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 v x Hv1 Hx Hv2.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
Apply L6 w Hw to the current goal.
Let w' be given.
Assume Hw'.
Apply Hw' to the current goal.
Assume Hw'1: w' ∈ L.
Assume Hw'2: w ≤ w'.
We prove the intermediate claim Lw': SNo w'.
An exact proof term for the current goal is HL w' Hw'1.
We prove the intermediate claim Lxw': SNo (x * w').
An exact proof term for the current goal is SNo_mul_SNo x w' Hx Lw'.
We prove the intermediate claim Lvpos: 0 < v.
Apply SNoLtLe_or 0 v SNo_0 Hv1 to the current goal.
Assume H8: 0 < v.
An exact proof term for the current goal is H8.
Assume H8: v ≤ 0.
We will prove False.
Apply SNoLt_irref 1 to the current goal.
We will prove 1 < 1.
Apply SNoLeLt_tra 1 (x * w') 1 SNo_1 Lxw' SNo_1 to the current goal.
We will prove 1 ≤ x * w'.
Apply SNoLe_tra 1 (x * w) (x * w') SNo_1 Lxw Lxw' to the current goal.
We will prove 1 ≤ x * w.
Apply SNoLe_tra 1 (v * (y + - w) + x * w) (x * w) SNo_1 (SNo_add_SNo (v * (y + - w)) (x * w) (SNo_mul_SNo v (y + - w) Hv1 (SNo_add_SNo y (- w) H1 (SNo_minus_SNo w Hw1))) Lxw) Lxw to the current goal.
We will prove 1 ≤ v * (y + - w) + x * w.
rewrite the current goal using mul_SNo_distrL v y (- w) Hv1 H1 (SNo_minus_SNo w Hw1) (from left to right).
We will prove 1 ≤ (v * y + v * (- w)) + x * w.
rewrite the current goal using add_SNo_com_3b_1_2 (v * y) (v * (- w)) (x * w) (SNo_mul_SNo v y Hv1 H1) (SNo_mul_SNo v (- w) Hv1 (SNo_minus_SNo w Hw1)) Lxw (from left to right).
We will prove 1 ≤ (v * y + x * w) + v * (- w).
rewrite the current goal using mul_SNo_minus_distrR v w Hv1 Hw1 (from left to right).
We will prove 1 ≤ (v * y + x * w) + - v * w.
Apply add_SNo_minus_Le2b (v * y + x * w) (v * w) 1 (SNo_add_SNo (v * y) (x * w) (SNo_mul_SNo v y Hv1 H1) Lxw) (SNo_mul_SNo v w Hv1 Hw1) SNo_1 to the current goal.
We will prove 1 + v * w ≤ v * y + x * w.
An exact proof term for the current goal is H7.
We will prove v * (y + - w) + x * w ≤ x * w.
rewrite the current goal using add_SNo_0L (x * w) Lxw (from right to left) at position 2.
We will prove v * (y + - w) + x * w ≤ 0 + x * w.
Apply add_SNo_Le1 (v * (y + - w)) (x * w) 0 (SNo_mul_SNo v (y + - w) Hv1 (SNo_add_SNo y (- w) H1 (SNo_minus_SNo w Hw1))) Lxw SNo_0 to the current goal.
We will prove v * (y + - w) ≤ 0.
Apply mul_SNo_nonpos_pos v (y + - w) Hv1 (SNo_add_SNo y (- w) H1 (SNo_minus_SNo w Hw1)) H8 to the current goal.
We will prove 0 < y + - w.
Apply add_SNo_minus_Lt2b y w 0 H1 Hw1 SNo_0 to the current goal.
We will prove 0 + w < y.
rewrite the current goal using add_SNo_0L w Hw1 (from left to right).
We will prove w < y.
An exact proof term for the current goal is Hw3.
We will prove x * w ≤ x * w'.
An exact proof term for the current goal is nonneg_mul_SNo_Le x w w' Hx (SNoLtLe 0 x Hxpos) Hw1 Lw' Hw'2.
We will prove x * w' < 1.
An exact proof term for the current goal is L1L w' Hw'1.
Set w'' to be the term (1 + (v + - x) * w') * recip_SNo_pos v.
We prove the intermediate claim Lw'': w'' ∈ R.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) w' Hw'1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H9: w' ∈ SNo_recipaux x recip_SNo_pos k 0.
Apply famunionI ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 1) (ordsucc k) w'' (omega_ordsucc k Hk) to the current goal.
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos (ordsucc k) 1.
rewrite the current goal using SNo_recipaux_S x recip_SNo_pos k (omega_nat_p k Hk) (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos k 1 ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoL_pos x) recip_SNo_pos ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoR x) recip_SNo_pos.
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
We will prove w'' ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoL_pos x) recip_SNo_pos.
Apply SNo_recipauxset_I (SNo_recipaux x recip_SNo_pos k 0) x (SNoL_pos x) recip_SNo_pos to the current goal.
We will prove w' ∈ SNo_recipaux x recip_SNo_pos k 0.
An exact proof term for the current goal is H9.
We will prove v ∈ SNoL_pos x.
We will prove v ∈ {w ∈ SNoL x|0 < w}.
Apply SepI to the current goal.
An exact proof term for the current goal is Hv.
We will prove 0 < v.
An exact proof term for the current goal is Lvpos.
Apply L11 v w w' Hv1 Hw1 Lw' LvS Lvpos H7 Lw'' to the current goal.
We will prove (- v + x) * w ≤ (- v + x) * w'.
Apply nonneg_mul_SNo_Le (- v + x) w w' (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) to the current goal.
We will prove 0 ≤ - v + x.
rewrite the current goal using add_SNo_com (- v) x (SNo_minus_SNo v Hv1) Hx (from left to right).
We will prove 0 ≤ x + - v.
Apply add_SNo_minus_Le2b x v 0 Hx Hv1 SNo_0 to the current goal.
We will prove 0 + v ≤ x.
rewrite the current goal using add_SNo_0L v Hv1 (from left to right).
We will prove v ≤ x.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hv3.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is Lw'.
An exact proof term for the current goal is Hw'2.
Let v be given.
Assume Hv: v ∈ SNoR x.
Let w be given.
Assume Hw: w ∈ SNoR y.
Assume H7: 1 + v * w ≤ v * y + x * w.
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: x < v.
Apply SNoR_E y H1 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: y < w.
We prove the intermediate claim LvS: v ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 v x Hv1 Hx Hv2.
We prove the intermediate claim Lvpos: 0 < v.
An exact proof term for the current goal is SNoLt_tra 0 x v SNo_0 Hx Hv1 Hxpos Hv3.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
Apply L7 w Hw to the current goal.
Let w' be given.
Assume Hw'.
Apply Hw' to the current goal.
Assume Hw'1: w' ∈ R.
Assume Hw'2: w' ≤ w.
We prove the intermediate claim Lw': SNo w'.
An exact proof term for the current goal is HR w' Hw'1.
We prove the intermediate claim Lxw': SNo (x * w').
An exact proof term for the current goal is SNo_mul_SNo x w' Hx Lw'.
Set w'' to be the term (1 + (v + - x) * w') * recip_SNo_pos v.
We prove the intermediate claim Lw'': w'' ∈ R.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 1) w' Hw'1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H9: w' ∈ SNo_recipaux x recip_SNo_pos k 1.
Apply famunionI ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 1) (ordsucc k) w'' (omega_ordsucc k Hk) to the current goal.
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos (ordsucc k) 1.
rewrite the current goal using SNo_recipaux_S x recip_SNo_pos k (omega_nat_p k Hk) (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos k 1 ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoL_pos x) recip_SNo_pos ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoR x) recip_SNo_pos.
Apply binunionI2 to the current goal.
We will prove w'' ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoR x) recip_SNo_pos.
Apply SNo_recipauxset_I (SNo_recipaux x recip_SNo_pos k 1) x (SNoR x) recip_SNo_pos to the current goal.
We will prove w' ∈ SNo_recipaux x recip_SNo_pos k 1.
An exact proof term for the current goal is H9.
We will prove v ∈ SNoR x.
An exact proof term for the current goal is Hv.
Apply L11 v w w' Hv1 Hw1 Lw' LvS Lvpos H7 Lw'' to the current goal.
We will prove (- v + x) * w ≤ (- v + x) * w'.
Apply L11 v w w' Hv1 Hw1 Lw' LvS Lvpos H7 Lw'' to the current goal.
We will prove (- v + x) * w ≤ (- v + x) * w'.
Apply nonpos_mul_SNo_Le (- v + x) w w' (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) to the current goal.
We will prove - v + x ≤ 0.
rewrite the current goal using add_SNo_com (- v) x (SNo_minus_SNo v Hv1) Hx (from left to right).
We will prove x + - v ≤ 0.
Apply add_SNo_minus_Le2 0 (- v) x SNo_0 (SNo_minus_SNo v Hv1) Hx to the current goal.
rewrite the current goal using minus_SNo_invol v Hv1 (from left to right).
We will prove x ≤ 0 + v.
rewrite the current goal using add_SNo_0L v Hv1 (from left to right).
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hv3.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is Lw'.
An exact proof term for the current goal is Hw'2.
∎
Theorem. (SNo_recip_SNo_pos)
∀x, SNo x → 0 < x → SNo (recip_SNo_pos x)
In Proofgold the corresponding term root is 90e6e6... and proposition id is 6b9294...
Proof:
Let x be given.
Assume Hx Hxpos.
Apply recip_SNo_pos_prop1 x Hx Hxpos to the current goal.
Assume H _.
An exact proof term for the current goal is H.
∎
Theorem. (recip_SNo_pos_invR)
∀x, SNo x → 0 < x → x * recip_SNo_pos x = 1
In Proofgold the corresponding term root is 12c412... and proposition id is a4f83c...
Proof:
Let x be given.
Assume Hx Hxpos.
Apply recip_SNo_pos_prop1 x Hx Hxpos to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
∎
Theorem. (recip_SNo_pos_1)
recip_SNo_pos 1 = 1
In Proofgold the corresponding term root is df53e8... and proposition id is bf8279...
Proof:
Apply mul_SNo_nonzero_cancel 1 (recip_SNo_pos 1) 1 SNo_1 neq_1_0 (SNo_recip_SNo_pos 1 SNo_1 SNoLt_0_1) SNo_1 to the current goal.
We will prove 1 * recip_SNo_pos 1 = 1 * 1.
rewrite the current goal using mul_SNo_oneL 1 SNo_1 (from left to right).
We will prove 1 * recip_SNo_pos 1 = 1.
An exact proof term for the current goal is recip_SNo_pos_invR 1 SNo_1 SNoLt_0_1.
∎
Theorem. (recip_SNo_pos_is_pos)
∀x, SNo x → 0 < x → 0 < recip_SNo_pos x
In Proofgold the corresponding term root is c95744... and proposition id is 30d6a5...
Proof:
Let x be given.
Assume Hx Hxpos.
We prove the intermediate claim Lrx: SNo (recip_SNo_pos x).
An exact proof term for the current goal is SNo_recip_SNo_pos x Hx Hxpos.
Apply SNoLt_trichotomy_or_impred (recip_SNo_pos x) 0 Lrx SNo_0 to the current goal.
Assume H1: recip_SNo_pos x < 0.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
Apply SNoLt_tra 0 1 0 SNo_0 SNo_1 SNo_0 SNoLt_0_1 to the current goal.
We will prove 1 < 0.
rewrite the current goal using recip_SNo_pos_invR x Hx Hxpos (from right to left).
We will prove x * recip_SNo_pos x < 0.
An exact proof term for the current goal is mul_SNo_pos_neg x (recip_SNo_pos x) Hx Lrx Hxpos H1.
Assume H1: recip_SNo_pos x = 0.
We will prove False.
Apply neq_1_0 to the current goal.
We will prove 1 = 0.
rewrite the current goal using recip_SNo_pos_invR x Hx Hxpos (from right to left).
We will prove x * recip_SNo_pos x = 0.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is mul_SNo_zeroR x Hx.
Assume H1.
An exact proof term for the current goal is H1.
∎
Theorem. (recip_SNo_pos_invol)
∀x, SNo x → 0 < x → recip_SNo_pos (recip_SNo_pos x) = x
In Proofgold the corresponding term root is 5e7409... and proposition id is a3c6c5...
Proof:
Let x be given.
Assume Hx Hxpos.
We prove the intermediate claim Lrx: SNo (recip_SNo_pos x).
An exact proof term for the current goal is SNo_recip_SNo_pos x Hx Hxpos.
We prove the intermediate claim Lrxpos: 0 < recip_SNo_pos x.
An exact proof term for the current goal is recip_SNo_pos_is_pos x Hx Hxpos.
We prove the intermediate claim Lrrx: SNo (recip_SNo_pos (recip_SNo_pos x)).
An exact proof term for the current goal is SNo_recip_SNo_pos (recip_SNo_pos x) Lrx Lrxpos.
We prove the intermediate claim Lrxn0: recip_SNo_pos x ≠ 0.
Assume Hrx0: recip_SNo_pos x = 0.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
rewrite the current goal using Hrx0 (from right to left) at position 2.
An exact proof term for the current goal is Lrxpos.
We will prove recip_SNo_pos (recip_SNo_pos x) = x.
Apply mul_SNo_nonzero_cancel (recip_SNo_pos x) (recip_SNo_pos (recip_SNo_pos x)) x Lrx Lrxn0 Lrrx Hx to the current goal.
We will prove recip_SNo_pos x * recip_SNo_pos (recip_SNo_pos x) = recip_SNo_pos x * x.
rewrite the current goal using mul_SNo_com (recip_SNo_pos x) x Lrx Hx (from left to right).
rewrite the current goal using recip_SNo_pos_invR x Hx Hxpos (from left to right).
An exact proof term for the current goal is recip_SNo_pos_invR (recip_SNo_pos x) Lrx Lrxpos.
∎
Theorem. (recip_SNo_pos_eps_)
∀n, nat_p n → recip_SNo_pos (eps_ n) = 2 ^ n
In Proofgold the corresponding term root is ce7e5d... and proposition id is 3c7219...
Proof:
Let n be given.
Assume Hn.
We prove the intermediate claim Len1: SNo (eps_ n).
An exact proof term for the current goal is SNo_eps_ n (nat_p_omega n Hn).
We prove the intermediate claim Len2: 0 < eps_ n.
An exact proof term for the current goal is SNo_eps_pos n (nat_p_omega n Hn).
We prove the intermediate claim Len3: eps_ n ≠ 0.
Assume H1: eps_ n = 0.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
rewrite the current goal using H1 (from right to left) at position 2.
We will prove 0 < eps_ n.
An exact proof term for the current goal is Len2.
Apply mul_SNo_nonzero_cancel (eps_ n) (recip_SNo_pos (eps_ n)) (2 ^ n) Len1 Len3 (SNo_recip_SNo_pos (eps_ n) Len1 Len2) (SNo_exp_SNo_nat 2 SNo_2 n Hn) to the current goal.
We will prove eps_ n * recip_SNo_pos (eps_ n) = eps_ n * 2 ^ n.
rewrite the current goal using mul_SNo_eps_power_2 n Hn (from left to right).
We will prove eps_ n * recip_SNo_pos (eps_ n) = 1.
An exact proof term for the current goal is recip_SNo_pos_invR (eps_ n) Len1 Len2.
∎
Theorem. (recip_SNo_pos_pow_2)
∀n, nat_p n → recip_SNo_pos (2 ^ n) = eps_ n
In Proofgold the corresponding term root is e4f02a... and proposition id is 9ca0e9...
Proof:
Let n be given.
Assume Hn.
rewrite the current goal using recip_SNo_pos_eps_ n Hn (from right to left).
An exact proof term for the current goal is recip_SNo_pos_invol (eps_ n) (SNo_eps_ n (nat_p_omega n Hn)) (SNo_eps_pos n (nat_p_omega n Hn)).
∎
Theorem. (recip_SNo_pos_2)
recip_SNo_pos 2 = eps_ 1
In Proofgold the corresponding term root is 1953c2... and proposition id is 4addd0...
Proof:
rewrite the current goal using exp_SNo_nat_1 2 SNo_2 (from right to left).
An exact proof term for the current goal is recip_SNo_pos_pow_2 1 nat_1.
∎
End of Section recip_SNo_pos
Definition. We define recip_SNo to be λx ⇒ if 0 < x then recip_SNo_pos x else if x < 0 then - recip_SNo_pos (- x) else 0 of type set → set.
In Proofgold the corresponding term root is aa96a2... and object id is 0d39b7...
Theorem. (recip_SNo_poscase)
∀x, 0 < x → recip_SNo x = recip_SNo_pos x
In Proofgold the corresponding term root is 152688... and proposition id is 2f43fd...
Proof:
Let x be given.
Assume Hxpos.
An exact proof term for the current goal is If_i_1 (0 < x) (recip_SNo_pos x) (if x < 0 then - recip_SNo_pos (- x) else 0) Hxpos.
∎
Theorem. (recip_SNo_negcase)
∀x, SNo x → x < 0 → recip_SNo x = - recip_SNo_pos (- x)
In Proofgold the corresponding term root is c96182... and proposition id is 126cc9...
Proof:
Let x be given.
Assume Hx Hxneg.
We prove the intermediate claim L1: ¬ (0 < x).
Assume H1.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
An exact proof term for the current goal is SNoLt_tra 0 x 0 SNo_0 Hx SNo_0 H1 Hxneg.
We will prove (if 0 < x then recip_SNo_pos x else if x < 0 then - recip_SNo_pos (- x) else 0) = - recip_SNo_pos (- x).
rewrite the current goal using If_i_0 (0 < x) (recip_SNo_pos x) (if x < 0 then - recip_SNo_pos (- x) else 0) L1 (from left to right).
An exact proof term for the current goal is If_i_1 (x < 0) (- recip_SNo_pos (- x)) 0 Hxneg.
∎
Theorem. (recip_SNo_0)
recip_SNo 0 = 0
In Proofgold the corresponding term root is bda1b2... and proposition id is 466dab...
Proof:
We will prove (if 0 < 0 then recip_SNo_pos 0 else if 0 < 0 then - recip_SNo_pos (- 0) else 0) = 0.
rewrite the current goal using If_i_0 (0 < 0) (recip_SNo_pos 0) (if 0 < 0 then - recip_SNo_pos (- 0) else 0) (SNoLt_irref 0) (from left to right).
We will prove (if 0 < 0 then - recip_SNo_pos (- 0) else 0) = 0.
An exact proof term for the current goal is If_i_0 (0 < 0) (- recip_SNo_pos (- 0)) 0 (SNoLt_irref 0).
∎
Theorem. (recip_SNo_1)
recip_SNo 1 = 1
In Proofgold the corresponding term root is cb7d70... and proposition id is 75c888...
Proof:
rewrite the current goal using recip_SNo_poscase 1 SNoLt_0_1 (from left to right).
An exact proof term for the current goal is recip_SNo_pos_1.
∎
Theorem. (SNo_recip_SNo)
∀x, SNo x → SNo (recip_SNo x)
In Proofgold the corresponding term root is 675572... and proposition id is 9f0369...
Proof:
Let x be given.
Assume Hx.
Apply SNoLt_trichotomy_or_impred x 0 Hx SNo_0 to the current goal.
Assume H1: x < 0.
rewrite the current goal using recip_SNo_negcase x Hx H1 (from left to right).
We will prove SNo (- recip_SNo_pos (- x)).
Apply SNo_minus_SNo to the current goal.
We will prove SNo (recip_SNo_pos (- x)).
Apply SNo_recip_SNo_pos to the current goal.
An exact proof term for the current goal is SNo_minus_SNo x Hx.
We will prove 0 < - x.
Apply minus_SNo_Lt_contra2 x 0 Hx SNo_0 to the current goal.
We will prove x < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
We will prove x < 0.
An exact proof term for the current goal is H1.
Assume H1: x = 0.
rewrite the current goal using H1 (from left to right).
rewrite the current goal using recip_SNo_0 (from left to right).
An exact proof term for the current goal is SNo_0.
Assume H1: 0 < x.
rewrite the current goal using recip_SNo_poscase x H1 (from left to right).
An exact proof term for the current goal is SNo_recip_SNo_pos x Hx H1.
∎
Theorem. (recip_SNo_invR)
∀x, SNo x → x ≠ 0 → x * recip_SNo x = 1
In Proofgold the corresponding term root is 33c26e... and proposition id is 446f16...
Proof:
Let x be given.
Assume Hx Hx0.
Apply SNoLt_trichotomy_or_impred x 0 Hx SNo_0 to the current goal.
Assume H1: x < 0.
rewrite the current goal using recip_SNo_negcase x Hx H1 (from left to right).
We prove the intermediate claim L1: 0 < - x.
Apply minus_SNo_Lt_contra2 x 0 Hx SNo_0 to the current goal.
We will prove x < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
We will prove x < 0.
An exact proof term for the current goal is H1.
We will prove x * (- recip_SNo_pos (- x)) = 1.
rewrite the current goal using mul_SNo_minus_distrR x (recip_SNo_pos (- x)) Hx (SNo_recip_SNo_pos (- x) (SNo_minus_SNo x Hx) L1) (from left to right).
We will prove - (x * recip_SNo_pos (- x)) = 1.
rewrite the current goal using mul_SNo_minus_distrL x (recip_SNo_pos (- x)) Hx (SNo_recip_SNo_pos (- x) (SNo_minus_SNo x Hx) L1) (from right to left).
We will prove (- x) * recip_SNo_pos (- x) = 1.
An exact proof term for the current goal is recip_SNo_pos_invR (- x) (SNo_minus_SNo x Hx) L1.
Assume H1: x = 0.
We will prove False.
An exact proof term for the current goal is Hx0 H1.
Assume H1: 0 < x.
rewrite the current goal using recip_SNo_poscase x H1 (from left to right).
An exact proof term for the current goal is recip_SNo_pos_invR x Hx H1.
∎
Theorem. (recip_SNo_invL)
∀x, SNo x → x ≠ 0 → recip_SNo x * x = 1
In Proofgold the corresponding term root is 85d435... and proposition id is e80fdb...
Proof:
Let x be given.
Assume Hx Hx0.
rewrite the current goal using mul_SNo_com (recip_SNo x) x (SNo_recip_SNo x Hx) Hx (from left to right).
We will prove x * recip_SNo x = 1.
An exact proof term for the current goal is recip_SNo_invR x Hx Hx0.
∎
Theorem. (recip_SNo_eps_)
∀n, nat_p n → recip_SNo (eps_ n) = 2 ^ n
In Proofgold the corresponding term root is bbfaeb... and proposition id is 811e50...
Proof:
Let n be given.
Assume Hn.
rewrite the current goal using recip_SNo_poscase (eps_ n) (SNo_eps_pos n (nat_p_omega n Hn)) (from left to right).
An exact proof term for the current goal is recip_SNo_pos_eps_ n Hn.
∎
Theorem. (recip_SNo_pow_2)
∀n, nat_p n → recip_SNo (2 ^ n) = eps_ n
In Proofgold the corresponding term root is 761b63... and proposition id is 80f328...
Proof:
Let n be given.
Assume Hn.
We prove the intermediate claim L1: 0 < 2 ^ n.
An exact proof term for the current goal is exp_SNo_nat_pos 2 SNo_2 SNoLt_0_2 n Hn.
rewrite the current goal using recip_SNo_poscase (2 ^ n) L1 (from left to right).
An exact proof term for the current goal is recip_SNo_pos_pow_2 n Hn.
∎
Theorem. (recip_SNo_2)
recip_SNo 2 = eps_ 1
In Proofgold the corresponding term root is 1a7547... and proposition id is c21d28...
Proof:
rewrite the current goal using recip_SNo_poscase 2 SNoLt_0_2 (from left to right).
An exact proof term for the current goal is recip_SNo_pos_2.
∎
Theorem. (recip_SNo_invol)
∀x, SNo x → recip_SNo (recip_SNo x) = x
In Proofgold the corresponding term root is d2c4c3... and proposition id is f0af46...
Proof:
Let x be given.
Assume Hx.
Apply SNoLt_trichotomy_or_impred x 0 Hx SNo_0 to the current goal.
Assume H1: x < 0.
rewrite the current goal using recip_SNo_negcase x Hx H1 (from left to right).
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
We prove the intermediate claim Lmxpos: 0 < - x.
Apply minus_SNo_Lt_contra2 x 0 Hx SNo_0 to the current goal.
We will prove x < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
We will prove x < 0.
An exact proof term for the current goal is H1.
We prove the intermediate claim Lrmx: SNo (recip_SNo_pos (- x)).
An exact proof term for the current goal is SNo_recip_SNo_pos (- x) Lmx Lmxpos.
We prove the intermediate claim Lmrmx: SNo (- recip_SNo_pos (- x)).
An exact proof term for the current goal is SNo_minus_SNo (recip_SNo_pos (- x)) Lrmx.
We prove the intermediate claim L1: 0 < recip_SNo_pos (- x).
An exact proof term for the current goal is recip_SNo_pos_is_pos (- x) Lmx Lmxpos.
We prove the intermediate claim L2: - recip_SNo_pos (- x) < 0.
Apply minus_SNo_Lt_contra1 0 (recip_SNo_pos (- x)) SNo_0 Lrmx to the current goal.
We will prove - 0 < recip_SNo_pos (- x).
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is L1.
rewrite the current goal using recip_SNo_negcase (- (recip_SNo_pos (- x))) Lmrmx L2 (from left to right).
We will prove - recip_SNo_pos (- (- (recip_SNo_pos (- x)))) = x.
rewrite the current goal using minus_SNo_invol (recip_SNo_pos (- x)) Lrmx (from left to right).
rewrite the current goal using recip_SNo_pos_invol (- x) Lmx Lmxpos (from left to right).
An exact proof term for the current goal is minus_SNo_invol x Hx.
Assume H1: x = 0.
rewrite the current goal using H1 (from left to right).
rewrite the current goal using recip_SNo_0 (from left to right).
An exact proof term for the current goal is recip_SNo_0.
Assume H1: 0 < x.
rewrite the current goal using recip_SNo_poscase x H1 (from left to right).
rewrite the current goal using recip_SNo_poscase (recip_SNo_pos x) (recip_SNo_pos_is_pos x Hx H1) (from left to right).
An exact proof term for the current goal is recip_SNo_pos_invol x Hx H1.
∎
Theorem. (recip_SNo_of_pos_is_pos)
∀x, SNo x → 0 < x → 0 < recip_SNo x
In Proofgold the corresponding term root is 8f5692... and proposition id is 1015d4...
Proof:
Let x be given.
Assume Hx Hxpos.
rewrite the current goal using recip_SNo_poscase x Hxpos (from left to right).
An exact proof term for the current goal is recip_SNo_pos_is_pos x Hx Hxpos.
∎
Theorem. (recip_SNo_neg')
∀x, SNo x → x < 0 → recip_SNo x < 0
In Proofgold the corresponding term root is eceae8... and proposition id is 49b9ec...
Proof:
Let x be given.
Assume Hx Hxneg.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
We prove the intermediate claim Lmxpos: 0 < - x.
Apply minus_SNo_Lt_contra2 x 0 Hx SNo_0 to the current goal.
We will prove x < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is Hxneg.
We prove the intermediate claim Lrmx: SNo (recip_SNo_pos (- x)).
Apply SNo_recip_SNo_pos to the current goal.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Lmxpos.
rewrite the current goal using recip_SNo_negcase x Hx Hxneg (from left to right).
We will prove - recip_SNo_pos (- x) < 0.
Apply minus_SNo_Lt_contra1 0 (recip_SNo_pos (- x)) SNo_0 Lrmx to the current goal.
We will prove - 0 < recip_SNo_pos (- x).
rewrite the current goal using minus_SNo_0 (from left to right).
We will prove 0 < recip_SNo_pos (- x).
Apply recip_SNo_pos_is_pos (- x) Lmx to the current goal.
We will prove 0 < - x.
An exact proof term for the current goal is Lmxpos.
∎
Definition. We define div_SNo to be λx y ⇒ x * recip_SNo y of type set → set → set.
In Proofgold the corresponding term root is a77cc8... and object id is 8b12fd...
Notation. We use :/: as an infix operator with priority 353 and no associativity corresponding to applying term div_SNo.
Theorem. (SNo_div_SNo)
∀x y, SNo x → SNo y → SNo (x :/: y)
In Proofgold the corresponding term root is cebe75... and proposition id is c761b5...
Proof:
Let x and y be given.
Assume Hx Hy.
We will prove SNo (x * recip_SNo y).
An exact proof term for the current goal is SNo_mul_SNo x (recip_SNo y) Hx (SNo_recip_SNo y Hy).
∎
Theorem. (div_SNo_0_num)
∀x, SNo x → 0 :/: x = 0
In Proofgold the corresponding term root is 28c3dc... and proposition id is ec5f74...
Proof:
Let x be given.
Assume Hx.
An exact proof term for the current goal is mul_SNo_zeroL (recip_SNo x) (SNo_recip_SNo x Hx).
∎
Theorem. (div_SNo_0_denum)
∀x, SNo x → x :/: 0 = 0
In Proofgold the corresponding term root is d6eb4e... and proposition id is 46b3d2...
Proof:
Let x be given.
Assume Hx.
We will prove x * recip_SNo 0 = 0.
rewrite the current goal using recip_SNo_0 (from left to right).
An exact proof term for the current goal is mul_SNo_zeroR x Hx.
∎
Theorem. (mul_div_SNo_invL)
∀x y, SNo x → SNo y → y ≠ 0 → (x :/: y) * y = x
In Proofgold the corresponding term root is 2484b5... and proposition id is 07d80b...
Proof:
Let x and y be given.
Assume Hx Hy Hy0.
We will prove (x * recip_SNo y) * y = x.
rewrite the current goal using mul_SNo_assoc x (recip_SNo y) y Hx (SNo_recip_SNo y Hy) Hy (from right to left).
We will prove x * (recip_SNo y * y) = x.
rewrite the current goal using recip_SNo_invL y Hy Hy0 (from left to right).
We will prove x * 1 = x.
An exact proof term for the current goal is mul_SNo_oneR x Hx.
∎
Theorem. (mul_div_SNo_invR)
∀x y, SNo x → SNo y → y ≠ 0 → y * (x :/: y) = x
In Proofgold the corresponding term root is 9b260e... and proposition id is df334a...
Proof:
Let x and y be given.
Assume Hx Hy Hy0.
rewrite the current goal using mul_SNo_com y (x :/: y) Hy (SNo_div_SNo x y Hx Hy) (from left to right).
An exact proof term for the current goal is mul_div_SNo_invL x y Hx Hy Hy0.
∎
Theorem. (mul_div_SNo_R)
∀x y z, SNo x → SNo y → SNo z → (x :/: y) * z = (x * z) :/: y
In Proofgold the corresponding term root is a78538... and proposition id is daa8eb...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
Apply xm (y = 0) to the current goal.
Assume H1: y = 0.
rewrite the current goal using H1 (from left to right).
rewrite the current goal using div_SNo_0_denum x Hx (from left to right).
rewrite the current goal using div_SNo_0_denum (x * z) (SNo_mul_SNo x z Hx Hz) (from left to right).
We will prove 0 * z = 0.
An exact proof term for the current goal is mul_SNo_zeroL z Hz.
Assume H1: y ≠ 0.
Apply mul_SNo_nonzero_cancel y ((x :/: y) * z) ((x * z) :/: y) Hy H1 (SNo_mul_SNo (x :/: y) z (SNo_div_SNo x y Hx Hy) Hz) (SNo_div_SNo (x * z) y (SNo_mul_SNo x z Hx Hz) Hy) to the current goal.
We will prove y * (x :/: y) * z = y * (x * z) :/: y.
rewrite the current goal using mul_div_SNo_invR (x * z) y (SNo_mul_SNo x z Hx Hz) Hy H1 (from left to right).
We will prove y * (x :/: y) * z = x * z.
rewrite the current goal using mul_SNo_assoc y (x :/: y) z Hy (SNo_div_SNo x y Hx Hy) Hz (from left to right).
We will prove (y * (x :/: y)) * z = x * z.
Use f_equal.
We will prove y * (x :/: y) = x.
An exact proof term for the current goal is mul_div_SNo_invR x y Hx Hy H1.
∎
Theorem. (mul_div_SNo_L)
∀x y z, SNo x → SNo y → SNo z → z * (x :/: y) = (z * x) :/: y
In Proofgold the corresponding term root is 95a4c6... and proposition id is c10e5c...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
Use transitivity with (x :/: y) * z, and (x * z) :/: y.
An exact proof term for the current goal is mul_SNo_com z (x :/: y) Hz (SNo_div_SNo x y Hx Hy).
An exact proof term for the current goal is mul_div_SNo_R x y z Hx Hy Hz.
Use f_equal.
An exact proof term for the current goal is mul_SNo_com x z Hx Hz.
∎
Theorem. (div_mul_SNo_invL)
∀x y, SNo x → SNo y → y ≠ 0 → (x * y) :/: y = x
In Proofgold the corresponding term root is c74971... and proposition id is b99cd5...
Proof:
Let x and y be given.
Assume Hx Hy Hy0.
rewrite the current goal using mul_div_SNo_R x y y Hx Hy Hy (from right to left).
We will prove (x :/: y) * y = x.
An exact proof term for the current goal is mul_div_SNo_invL x y Hx Hy Hy0.
∎
Theorem. (div_div_SNo)
∀x y z, SNo x → SNo y → SNo z → (x :/: y) :/: z = x :/: (y * z)
In Proofgold the corresponding term root is 3e9827... and proposition id is de0369...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz.
We prove the intermediate claim Lxdy: SNo (x :/: y).
An exact proof term for the current goal is SNo_div_SNo x y Hx Hy.
We prove the intermediate claim Lxdydz: SNo ((x :/: y) :/: z).
An exact proof term for the current goal is SNo_div_SNo (x :/: y) z Lxdy Hz.
We prove the intermediate claim Lxy: SNo (x * y).
An exact proof term for the current goal is SNo_mul_SNo x y Hx Hy.
We prove the intermediate claim Lyz: SNo (y * z).
An exact proof term for the current goal is SNo_mul_SNo y z Hy Hz.
We prove the intermediate claim Lxdyz: SNo (x :/: (y * z)).
An exact proof term for the current goal is SNo_div_SNo x (y * z) Hx Lyz.
Apply xm (y = 0) to the current goal.
Assume Hy0: y = 0.
rewrite the current goal using Hy0 (from left to right).
We will prove (x :/: 0) :/: z = x :/: (0 * z).
rewrite the current goal using mul_SNo_zeroL z Hz (from left to right).
rewrite the current goal using div_SNo_0_denum x Hx (from left to right).
We will prove 0 :/: z = 0.
An exact proof term for the current goal is div_SNo_0_num z Hz.
Assume Hy0: y ≠ 0.
Apply xm (z = 0) to the current goal.
Assume Hz0: z = 0.
rewrite the current goal using Hz0 (from left to right).
We will prove (x :/: y) :/: 0 = x :/: (y * 0).
rewrite the current goal using mul_SNo_zeroR y Hy (from left to right).
We will prove (x :/: y) :/: 0 = x :/: 0.
rewrite the current goal using div_SNo_0_denum x Hx (from left to right).
An exact proof term for the current goal is div_SNo_0_denum (x :/: y) Lxdy.
Assume Hz0: z ≠ 0.
We prove the intermediate claim Lyz0: y * z ≠ 0.
Assume H1: y * z = 0.
Apply Hz0 to the current goal.
We will prove z = 0.
Apply mul_SNo_nonzero_cancel y z 0 Hy Hy0 Hz SNo_0 to the current goal.
We will prove y * z = y * 0.
rewrite the current goal using mul_SNo_zeroR y Hy (from left to right).
An exact proof term for the current goal is H1.
Apply mul_SNo_nonzero_cancel z ((x :/: y) :/: z) (x :/: (y * z)) Hz Hz0 Lxdydz Lxdyz to the current goal.
rewrite the current goal using mul_div_SNo_invR (x :/: y) z Lxdy Hz Hz0 (from left to right).
We will prove x :/: y = z * (x :/: (y * z)).
Apply mul_SNo_nonzero_cancel y (x :/: y) (z * (x :/: (y * z))) Hy Hy0 Lxdy (SNo_mul_SNo z (x :/: (y * z)) Hz Lxdyz) to the current goal.
rewrite the current goal using mul_div_SNo_invR x y Hx Hy Hy0 (from left to right).
We will prove x = y * z * (x :/: (y * z)).
rewrite the current goal using mul_SNo_assoc y z (x :/: (y * z)) Hy Hz Lxdyz (from left to right).
Use symmetry.
An exact proof term for the current goal is mul_div_SNo_invR x (y * z) Hx Lyz Lyz0.
∎
Theorem. (mul_div_SNo_both)
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x :/: y) * (z :/: w) = (x * z) :/: (y * w)
In Proofgold the corresponding term root is 06b28b... and proposition id is e61f18...
Proof:
Let x, y, z and w be given.
Assume Hx Hy Hz Hw.
rewrite the current goal using mul_div_SNo_L z w (x :/: y) Hz Hw (SNo_div_SNo x y Hx Hy) (from left to right).
We will prove ((x :/: y) * z) :/: w = (x * z) :/: (y * w).
rewrite the current goal using mul_div_SNo_R 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 div_div_SNo (x * z) y w (SNo_mul_SNo x z Hx Hz) Hy Hw.
∎
Theorem. (recip_SNo_pos_pos)
∀x, SNo x → 0 < x → 0 < recip_SNo_pos x
In Proofgold the corresponding term root is c95744... and proposition id is 30d6a5...
Proof:
Let x be given.
Assume Hx Hxpos.
Apply SNoLtLe_or 0 (recip_SNo_pos x) SNo_0 (SNo_recip_SNo_pos x Hx Hxpos) to the current goal.
Assume H1: 0 < recip_SNo_pos x.
An exact proof term for the current goal is H1.
Assume H1: recip_SNo_pos x ≤ 0.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
Apply SNoLtLe_tra 0 1 0 SNo_0 SNo_1 SNo_0 SNoLt_0_1 to the current goal.
We will prove 1 ≤ 0.
rewrite the current goal using recip_SNo_pos_invR x Hx Hxpos (from right to left).
We will prove x * recip_SNo_pos x ≤ 0.
rewrite the current goal using mul_SNo_zeroR x Hx (from right to left).
We will prove x * recip_SNo_pos x ≤ x * 0.
An exact proof term for the current goal is nonneg_mul_SNo_Le x (recip_SNo_pos x) 0 Hx (SNoLtLe 0 x Hxpos) (SNo_recip_SNo_pos x Hx Hxpos) SNo_0 H1.
∎
Theorem. (recip_SNo_of_neg_is_neg)
∀x, SNo x → x < 0 → recip_SNo x < 0
In Proofgold the corresponding term root is eceae8... and proposition id is 49b9ec...
Proof:
Let x be given.
Assume Hx Hxneg.
rewrite the current goal using recip_SNo_negcase x Hx Hxneg (from left to right).
We will prove - recip_SNo_pos (- x) < 0.
We prove the intermediate claim Lmx: SNo (- x).
An exact proof term for the current goal is SNo_minus_SNo x Hx.
We prove the intermediate claim L1: 0 < - x.
Apply minus_SNo_Lt_contra2 x 0 Hx SNo_0 to the current goal.
We will prove x < - 0.
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is Hxneg.
Apply minus_SNo_Lt_contra1 0 (recip_SNo_pos (- x)) SNo_0 (SNo_recip_SNo_pos (- x) Lmx L1) to the current goal.
We will prove - 0 < recip_SNo_pos (- x).
rewrite the current goal using minus_SNo_0 (from left to right).
We will prove 0 < recip_SNo_pos (- x).
Apply recip_SNo_pos_pos (- x) (SNo_minus_SNo x Hx) to the current goal.
We will prove 0 < - x.
An exact proof term for the current goal is L1.
∎
Theorem. (div_SNo_pos_pos)
∀x y, SNo x → SNo y → 0 < x → 0 < y → 0 < x :/: y
In Proofgold the corresponding term root is acf73b... and proposition id is 9935dd...
Proof:
Let x and y be given.
Assume Hx Hy Hxpos Hypos.
We will prove 0 < x * recip_SNo y.
Apply mul_SNo_pos_pos x (recip_SNo y) Hx (SNo_recip_SNo y Hy) Hxpos to the current goal.
We will prove 0 < recip_SNo y.
An exact proof term for the current goal is recip_SNo_of_pos_is_pos y Hy Hypos.
∎
Theorem. (div_SNo_neg_neg)
∀x y, SNo x → SNo y → x < 0 → y < 0 → 0 < x :/: y
In Proofgold the corresponding term root is 92b216... and proposition id is 7268ee...
Proof:
Let x and y be given.
Assume Hx Hy Hxneg Hyneg.
We will prove 0 < x * recip_SNo y.
Apply mul_SNo_neg_neg x (recip_SNo y) Hx (SNo_recip_SNo y Hy) Hxneg to the current goal.
We will prove recip_SNo y < 0.
An exact proof term for the current goal is recip_SNo_neg' y Hy Hyneg.
∎
Theorem. (div_SNo_pos_neg)
∀x y, SNo x → SNo y → 0 < x → y < 0 → x :/: y < 0
In Proofgold the corresponding term root is 8b3bd2... and proposition id is d188d5...
Proof:
Let x and y be given.
Assume Hx Hy Hxpos Hyneg.
We will prove x * recip_SNo y < 0.
Apply mul_SNo_pos_neg x (recip_SNo y) Hx (SNo_recip_SNo y Hy) Hxpos to the current goal.
We will prove recip_SNo y < 0.
An exact proof term for the current goal is recip_SNo_neg' y Hy Hyneg.
∎
Theorem. (div_SNo_neg_pos)
∀x y, SNo x → SNo y → x < 0 → 0 < y → x :/: y < 0
In Proofgold the corresponding term root is ff8d4c... and proposition id is df8e4a...
Proof:
Let x and y be given.
Assume Hx Hy Hxneg Hypos.
We will prove x * recip_SNo y < 0.
Apply mul_SNo_neg_pos x (recip_SNo y) Hx (SNo_recip_SNo y Hy) Hxneg to the current goal.
We will prove 0 < recip_SNo y.
An exact proof term for the current goal is recip_SNo_of_pos_is_pos y Hy Hypos.
∎
Theorem. (div_SNo_pos_LtL)
∀x y z, SNo x → SNo y → SNo z → 0 < y → x < z * y → x :/: y < z
In Proofgold the corresponding term root is 6ffbf3... and proposition id is 87c1ac...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz Hypos.
Assume H1: x < z * y.
We will prove x :/: y < z.
rewrite the current goal using mul_SNo_oneR z Hz (from right to left).
We will prove x :/: y < z * 1.
We prove the intermediate claim Ly0: y ≠ 0.
Assume H2: y = 0.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
rewrite the current goal using H2 (from left to right) at position 1.
An exact proof term for the current goal is Hypos.
rewrite the current goal using recip_SNo_invR y Hy Ly0 (from right to left).
We will prove x * recip_SNo y < z * y * recip_SNo y.
rewrite the current goal using mul_SNo_assoc z y (recip_SNo y) Hz Hy (SNo_recip_SNo y Hy) (from left to right).
We will prove x * recip_SNo y < (z * y) * recip_SNo y.
Apply pos_mul_SNo_Lt' x (z * y) (recip_SNo y) Hx (SNo_mul_SNo z y Hz Hy) (SNo_recip_SNo y Hy) to the current goal.
We will prove 0 < recip_SNo y.
An exact proof term for the current goal is recip_SNo_of_pos_is_pos y Hy Hypos.
We will prove x < z * y.
An exact proof term for the current goal is H1.
∎
Theorem. (div_SNo_pos_LtR)
∀x y z, SNo x → SNo y → SNo z → 0 < y → z * y < x → z < x :/: y
In Proofgold the corresponding term root is caaa93... and proposition id is c36da0...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz Hypos.
Assume H1: z * y < x.
We will prove z < x :/: y.
rewrite the current goal using mul_SNo_oneR z Hz (from right to left).
We will prove z * 1 < x :/: y.
We prove the intermediate claim Ly0: y ≠ 0.
Assume H2: y = 0.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
rewrite the current goal using H2 (from left to right) at position 1.
An exact proof term for the current goal is Hypos.
rewrite the current goal using recip_SNo_invR y Hy Ly0 (from right to left).
We will prove z * y * recip_SNo y < x * recip_SNo y.
rewrite the current goal using mul_SNo_assoc z y (recip_SNo y) Hz Hy (SNo_recip_SNo y Hy) (from left to right).
We will prove (z * y) * recip_SNo y < x * recip_SNo y.
Apply pos_mul_SNo_Lt' (z * y) x (recip_SNo y) (SNo_mul_SNo z y Hz Hy) Hx (SNo_recip_SNo y Hy) to the current goal.
We will prove 0 < recip_SNo y.
An exact proof term for the current goal is recip_SNo_of_pos_is_pos y Hy Hypos.
We will prove z * y < x.
An exact proof term for the current goal is H1.
∎
Theorem. (div_SNo_pos_LtL')
∀x y z, SNo x → SNo y → SNo z → 0 < y → x :/: y < z → x < z * y
In Proofgold the corresponding term root is 6d81ed... and proposition id is de6389...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz Hypos.
Assume H1: x :/: y < z.
We will prove x < z * y.
rewrite the current goal using mul_SNo_oneR x Hx (from right to left).
We will prove x * 1 < z * y.
We prove the intermediate claim Ly0: y ≠ 0.
Assume H2: y = 0.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
rewrite the current goal using H2 (from left to right) at position 1.
An exact proof term for the current goal is Hypos.
rewrite the current goal using recip_SNo_invL y Hy Ly0 (from right to left).
We will prove x * (recip_SNo y * y) < z * y.
rewrite the current goal using mul_SNo_assoc x (recip_SNo y) y Hx (SNo_recip_SNo y Hy) Hy (from left to right).
We will prove (x * recip_SNo y) * y < z * y.
We will prove (x :/: y) * y < z * y.
An exact proof term for the current goal is pos_mul_SNo_Lt' (x :/: y) z y (SNo_div_SNo x y Hx Hy) Hz Hy Hypos H1.
∎
Theorem. (div_SNo_pos_LtR')
∀x y z, SNo x → SNo y → SNo z → 0 < y → z < x :/: y → z * y < x
In Proofgold the corresponding term root is 0c5a47... and proposition id is a7e3d6...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz Hypos.
Assume H1: z < x :/: y.
We will prove z * y < x.
rewrite the current goal using mul_SNo_oneR x Hx (from right to left).
We will prove z * y < x * 1.
We prove the intermediate claim Ly0: y ≠ 0.
Assume H2: y = 0.
Apply SNoLt_irref y to the current goal.
We will prove y < y.
rewrite the current goal using H2 (from left to right) at position 1.
An exact proof term for the current goal is Hypos.
rewrite the current goal using recip_SNo_invL y Hy Ly0 (from right to left).
We will prove z * y < x * (recip_SNo y * y).
rewrite the current goal using mul_SNo_assoc x (recip_SNo y) y Hx (SNo_recip_SNo y Hy) Hy (from left to right).
We will prove z * y < (x * recip_SNo y) * y.
We will prove z * y < (x :/: y) * y.
An exact proof term for the current goal is pos_mul_SNo_Lt' z (x :/: y) y Hz (SNo_div_SNo x y Hx Hy) Hy Hypos H1.
∎
Theorem. (mul_div_SNo_nonzero_eq)
∀x y z, SNo x → SNo y → SNo z → y ≠ 0 → x = y * z → x :/: y = z
In Proofgold the corresponding term root is 4c4da2... and proposition id is bea168...
Proof:
Let x, y and z be given.
Assume Hx Hy Hz Hy0 H1.
Apply mul_SNo_nonzero_cancel y (x :/: y) z Hy Hy0 (SNo_div_SNo x y Hx Hy) Hz to the current goal.
We will prove y * (x :/: y) = y * z.
rewrite the current goal using mul_div_SNo_invR x y Hx Hy Hy0 (from left to right).
An exact proof term for the current goal is H1.
∎
End of Section SurrealDiv