Real Numbers
From Parts 1 - 7
Notation . We use
¬ as a prefix operator with priority 700 corresponding to applying term
not .
Notation . We use
∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term
and .
Notation . We use
∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term
or .
Notation . We use
↔ as an infix operator with priority 805 and no associativity corresponding to applying term
iff .
Beginning of Section Eq
Variable A : SType
End of Section Eq
Notation . We use
= as an infix operator with priority 502 and no associativity corresponding to applying term
eq .
Notation . We use
≠ as an infix operator with priority 502 and no associativity corresponding to applying term
neq .
Beginning of Section FE
Variable A B : SType
Axiom. (func_ext ) We take the following as an axiom:
∀f g : A → B , (∀x : A , f x = g x ) → f = g
End of Section FE
Beginning of Section Ex
Variable A : SType
End of Section Ex
Notation . We use
∃ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex .
Notation . We use
∈ as an infix operator with priority 500 and no associativity corresponding to applying term
In . Furthermore, we may write
∀ x ∈ A , B to mean
∀ x : set, x ∈ A → B .
Notation . We use
⊆ as an infix operator with priority 500 and no associativity corresponding to applying term
Subq . Furthermore, we may write
∀ x ⊆ A , B to mean
∀ x : set, x ⊆ A → B .
Axiom. (set_ext ) We take the following as an axiom:
∀X Y : set , X ⊆ Y → Y ⊆ X → X = Y
Axiom. (In_ind ) We take the following as an axiom:
∀P : set → prop , (∀X : set , (∀x ∈ X , P x ) → P X ) → ∀X : set , P X
Notation . We use
∃ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex and handling ∈ or ⊆ ascriptions using
and .
Axiom. (UnionEq ) We take the following as an axiom:
∀X x, x ∈ ⋃ X ↔ ∃Y, x ∈ Y ∧ Y ∈ X
Notation .
{B | x ∈ A } is notation for
Repl A (λ x . B ).
Axiom. (ReplEq ) We take the following as an axiom:
∀A : set , ∀F : set → set , ∀y : set , y ∈ {F x |x ∈ A } ↔ ∃x ∈ A , y = F x
Axiom. (andI ) We take the following as an axiom:
∀A B : prop , A → B → A ∧ B
Axiom. (andEL ) We take the following as an axiom:
∀A B : prop , A ∧ B → A
Axiom. (andER ) We take the following as an axiom:
∀A B : prop , A ∧ B → B
Axiom. (orIL ) We take the following as an axiom:
∀A B : prop , A → A ∨ B
Axiom. (orIR ) We take the following as an axiom:
∀A B : prop , B → A ∨ B
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (and3I ) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
Axiom. (and3E ) We take the following as an axiom:
P1 ∧ P2 ∧ P3 → (∀p : prop , (P1 → P2 → P3 → p ) → p )
Axiom. (or3I1 ) We take the following as an axiom:
P1 → P1 ∨ P2 ∨ P3
Axiom. (or3I2 ) We take the following as an axiom:
P2 → P1 ∨ P2 ∨ P3
Axiom. (or3I3 ) We take the following as an axiom:
P3 → P1 ∨ P2 ∨ P3
Axiom. (or3E ) We take the following as an axiom:
P1 ∨ P2 ∨ P3 → (∀p : prop , (P1 → p ) → (P2 → p ) → (P3 → p ) → p )
Variable P4 : prop
Axiom. (and4I ) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
Variable P5 : prop
Axiom. (and5I ) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
End of Section PropN
Axiom. (iffI ) We take the following as an axiom:
∀A B : prop , (A → B ) → (B → A ) → (A ↔ B )
Axiom. (iffEL ) We take the following as an axiom:
∀A B : prop , (A ↔ B ) → A → B
Axiom. (iffER ) We take the following as an axiom:
∀A B : prop , (A ↔ B ) → B → A
Axiom. (iff_sym ) We take the following as an axiom:
∀A B : prop , (A ↔ B ) → (B ↔ A )
Axiom. (iff_trans ) We take the following as an axiom:
∀A B C : prop , (A ↔ B ) → (B ↔ C ) → (A ↔ C )
Axiom. (eq_i_tra ) We take the following as an axiom:
∀x y z, x = y → y = z → x = z
Axiom. (f_eq_i ) We take the following as an axiom:
∀f : set → set , ∀x y, x = y → f x = f y
Notation . We use
∉ as an infix operator with priority 502 and no associativity corresponding to applying term
nIn .
Axiom. (pred_ext ) We take the following as an axiom:
∀P Q : set → prop , (∀x, P x ↔ Q x ) → P = Q
Axiom. (prop_ext_2 ) We take the following as an axiom:
∀p q : prop , (p → q ) → (q → p ) → p = q
Axiom. (Subq_tra ) We take the following as an axiom:
∀X Y Z : set , X ⊆ Y → Y ⊆ Z → X ⊆ Z
Axiom. (UnionI ) We take the following as an axiom:
∀X x Y : set , x ∈ Y → Y ∈ X → x ∈ ⋃ X
Axiom. (UnionE ) We take the following as an axiom:
∀X x : set , x ∈ ⋃ X → ∃Y : set , x ∈ Y ∧ Y ∈ X
Axiom. (UnionE_impred ) We take the following as an axiom:
∀X x : set , x ∈ ⋃ X → ∀p : prop , (∀Y : set , x ∈ Y → Y ∈ X → p ) → p
Axiom. (PowerI ) We take the following as an axiom:
∀X Y : set , Y ⊆ X → Y ∈ 𝒫 X
Axiom. (PowerE ) We take the following as an axiom:
∀X Y : set , Y ∈ 𝒫 X → Y ⊆ X
Axiom. (xm ) We take the following as an axiom:
∀P : prop , P ∨ ¬ P
Axiom. (dneg ) We take the following as an axiom:
∀P : prop , ¬ ¬ P → P
Axiom. (ReplI ) We take the following as an axiom:
∀A : set , ∀F : set → set , ∀x : set , x ∈ A → F x ∈ {F x |x ∈ A }
Axiom. (ReplE ) We take the following as an axiom:
∀A : set , ∀F : set → set , ∀y : set , y ∈ {F x |x ∈ A } → ∃x ∈ A , y = F x
Axiom. (ReplE_impred ) We take the following as an axiom:
∀A : set , ∀F : set → set , ∀y : set , y ∈ {F x |x ∈ A } → ∀p : prop , (∀x : set , x ∈ A → y = F x → p ) → p
Axiom. (ReplE' ) We take the following as an axiom:
∀X, ∀f : set → set , ∀p : set → prop , (∀x ∈ X , p (f x ) ) → ∀y ∈ {f x |x ∈ X } , p y
Axiom. (ReplEq_ext_sub ) We take the following as an axiom:
∀X, ∀F G : set → set , (∀x ∈ X , F x = G x ) → {F x |x ∈ X } ⊆ {G x |x ∈ X }
Axiom. (ReplEq_ext ) We take the following as an axiom:
∀X, ∀F G : set → set , (∀x ∈ X , F x = G x ) → {F x |x ∈ X } = {G x |x ∈ X }
Axiom. (Repl_inv_eq ) We take the following as an axiom:
∀P : set → prop , ∀f g : set → set , (∀x, P x → g (f x ) = x ) → ∀X, (∀x ∈ X , P x ) → {g y |y ∈ {f x |x ∈ X } } = X
Axiom. (Repl_invol_eq ) We take the following as an axiom:
∀P : set → prop , ∀f : set → set , (∀x, P x → f (f x ) = x ) → ∀X, (∀x ∈ X , P x ) → {f y |y ∈ {f x |x ∈ X } } = X
Notation . if cond then T else E is notation corresponding to If_i type cond T E where type is the inferred type of T .
Axiom. (If_i_correct ) We take the following as an axiom:
∀p : prop , ∀x y : set , p ∧ (if p then x else y ) = x ∨ ¬ p ∧ (if p then x else y ) = y
Axiom. (If_i_0 ) We take the following as an axiom:
∀p : prop , ∀x y : set , ¬ p → (if p then x else y ) = y
Axiom. (If_i_1 ) We take the following as an axiom:
∀p : prop , ∀x y : set , p → (if p then x else y ) = x
Axiom. (If_i_or ) We take the following as an axiom:
∀p : prop , ∀x y : set , (if p then x else y ) = x ∨ (if p then x else y ) = y
Notation .
{x ,y } is notation for
UPair x y .
Axiom. (UPairE ) We take the following as an axiom:
∀x y z : set , x ∈ {y ,z } → x = y ∨ x = z
Notation .
{x } is notation for
Sing x .
Axiom. (SingI ) We take the following as an axiom:
∀x : set , x ∈ {x }
Axiom. (SingE ) We take the following as an axiom:
∀x y : set , y ∈ {x } → y = x
Notation . We use
∪ as an infix operator with priority 345 and which associates to the left corresponding to applying term
binunion .
Axiom. (binunionE ) We take the following as an axiom:
∀X Y z : set , z ∈ X ∪ Y → z ∈ X ∨ z ∈ Y
Axiom. (binunionE' ) We take the following as an axiom:
∀X Y z, ∀p : prop , (z ∈ X → p ) → (z ∈ Y → p ) → (z ∈ X ∪ Y → p )
Notation . We now use the set enumeration notation
{...,...,...} in general. If 0 elements are given, then
Empty is used to form the corresponding term. If 1 element is given, then
Sing is used to form the corresponding term. If 2 elements are given, then
UPair is used to form the corresponding term. If more than elements are given, then
SetAdjoin is used to reduce to the case with one fewer elements.
Notation . We use
⋃ x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
famunion .
Axiom. (famunionI ) We take the following as an axiom:
∀X : set , ∀F : (set → set ) , ∀x y : set , x ∈ X → y ∈ F x → y ∈ ⋃x ∈ X F x
Axiom. (famunionE ) We take the following as an axiom:
∀X : set , ∀F : (set → set ) , ∀y : set , y ∈ (⋃x ∈ X F x ) → ∃x ∈ X , y ∈ F x
Axiom. (famunionE_impred ) We take the following as an axiom:
∀X : set , ∀F : (set → set ) , ∀y : set , y ∈ (⋃x ∈ X F x ) → ∀p : prop , (∀x, x ∈ X → y ∈ F x → p ) → p
Beginning of Section SepSec
Variable X : set
Variable P : set → prop
Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z )
Let F : set → set ≝ λx ⇒ if P x then x else z
End of Section SepSec
Notation .
{x ∈ A | B } is notation for
Sep A (λ x . B ).
Axiom. (SepI ) We take the following as an axiom:
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ X → P x → x ∈ {x ∈ X |P x }
Axiom. (SepE ) We take the following as an axiom:
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ {x ∈ X |P x } → x ∈ X ∧ P x
Axiom. (SepE1 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ {x ∈ X |P x } → x ∈ X
Axiom. (SepE2 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ {x ∈ X |P x } → P x
Axiom. (Sep_Subq ) We take the following as an axiom:
∀X : set , ∀P : set → prop , {x ∈ X |P x } ⊆ X
Notation .
{B | x ∈ A , C } is notation for
ReplSep A (λ x . C ) (λ x . B ).
Axiom. (ReplSepI ) We take the following as an axiom:
∀X : set , ∀P : set → prop , ∀F : set → set , ∀x : set , x ∈ X → P x → F x ∈ {F x |x ∈ X , P x }
Axiom. (ReplSepE ) We take the following as an axiom:
∀X : set , ∀P : set → prop , ∀F : set → set , ∀y : set , y ∈ {F x |x ∈ X , P x } → ∃x : set , x ∈ X ∧ P x ∧ y = F x
Axiom. (ReplSepE_impred ) We take the following as an axiom:
∀X : set , ∀P : set → prop , ∀F : set → set , ∀y : set , y ∈ {F x |x ∈ X , P x } → ∀p : prop , (∀x ∈ X , P x → y = F x → p ) → p
Notation . We use
∩ as an infix operator with priority 340 and which associates to the left corresponding to applying term
binintersect .
Notation . We use
∖ as an infix operator with priority 350 and no associativity corresponding to applying term
setminus .
Axiom. (setminusI ) We take the following as an axiom:
∀X Y z, (z ∈ X ) → (z ∉ Y ) → z ∈ X ∖ Y
Axiom. (setminusE ) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y ) → z ∈ X ∧ z ∉ Y
Notation . Natural numbers 0,1,2,... are notation for the terms formed using
Empty as 0 and forming successors with
ordsucc .
Axiom. (cases_1 ) We take the following as an axiom:
∀i ∈ 1 , ∀p : set → prop , p 0 → p i
Axiom. (cases_2 ) We take the following as an axiom:
∀i ∈ 2 , ∀p : set → prop , p 0 → p 1 → p i
Axiom. (cases_3 ) We take the following as an axiom:
∀i ∈ 3 , ∀p : set → prop , p 0 → p 1 → p 2 → p i
Axiom. (ordinal_ind ) We take the following as an axiom:
∀p : set → prop , (∀alpha, ordinal alpha → (∀beta ∈ alpha , p beta ) → p alpha ) → ∀alpha, ordinal alpha → p alpha
Definition. We define inj to be
λX Y f ⇒ (∀u ∈ X , f u ∈ Y ) ∧ (∀u v ∈ X , f u = f v → u = v ) of type
set → set → (set → set ) → prop .
Definition. We define bij to be
λX Y f ⇒ (∀u ∈ X , f u ∈ Y ) ∧ (∀u v ∈ X , f u = f v → u = v ) ∧ (∀w ∈ Y , ∃u ∈ X , f u = w ) of type
set → set → (set → set ) → prop .
Axiom. (bijI ) We take the following as an axiom:
∀X Y, ∀f : set → set , (∀u ∈ X , f u ∈ Y ) → (∀u v ∈ X , f u = f v → u = v ) → (∀w ∈ Y , ∃u ∈ X , f u = w ) → bij X Y f
Axiom. (bijE ) We take the following as an axiom:
∀X Y, ∀f : set → set , bij X Y f → ∀p : prop , ((∀u ∈ X , f u ∈ Y ) → (∀u v ∈ X , f u = f v → u = v ) → (∀w ∈ Y , ∃u ∈ X , f u = w ) → p ) → p
Axiom. (surj_rinv ) We take the following as an axiom:
∀X Y, ∀f : set → set , (∀w ∈ Y , ∃u ∈ X , f u = w ) → ∀y ∈ Y , inv X f y ∈ X ∧ f (inv X f y ) = y
Axiom. (inj_linv ) We take the following as an axiom:
∀X, ∀f : set → set , (∀u v ∈ X , f u = f v → u = v ) → ∀x ∈ X , inv X f (f x ) = x
Axiom. (bij_comp ) We take the following as an axiom:
∀X Y Z : set , ∀f g : set → set , bij X Y f → bij Y Z g → bij X Z (λx ⇒ g (f x ) )
Beginning of Section SchroederBernstein
Axiom. (KnasterTarski_set ) We take the following as an axiom:
∀A, ∀F : set → set , (∀U ∈ 𝒫 A , F U ∈ 𝒫 A ) → (∀U V ∈ 𝒫 A , U ⊆ V → F U ⊆ F V ) → ∃Y ∈ 𝒫 A , F Y = Y
Axiom. (image_In_Power ) We take the following as an axiom:
∀A B, ∀f : set → set , (∀x ∈ A , f x ∈ B ) → ∀U ∈ 𝒫 A , {f x |x ∈ U } ∈ 𝒫 B
Axiom. (image_monotone ) We take the following as an axiom:
∀f : set → set , ∀U V, U ⊆ V → {f x |x ∈ U } ⊆ {f x |x ∈ V }
End of Section SchroederBernstein
Beginning of Section PigeonHole
End of Section PigeonHole
Axiom. (exandE_i ) We take the following as an axiom:
∀P Q : set → prop , (∃x, P x ∧ Q x ) → ∀r : prop , (∀x, P x → Q x → r ) → r
Axiom. (exandE_ii ) We take the following as an axiom:
∀P Q : (set → set ) → prop , (∃x : set → set , P x ∧ Q x ) → ∀p : prop , (∀x : set → set , P x → Q x → p ) → p
Axiom. (exandE_iii ) We take the following as an axiom:
∀P Q : (set → set → set ) → prop , (∃x : set → set → set , P x ∧ Q x ) → ∀p : prop , (∀x : set → set → set , P x → Q x → p ) → p
Axiom. (exandE_iiii ) We take the following as an axiom:
∀P Q : (set → set → set → set ) → prop , (∃x : set → set → set → set , P x ∧ Q x ) → ∀p : prop , (∀x : set → set → set → set , P x → Q x → p ) → p
Beginning of Section Descr_ii
Variable P : (set → set ) → prop
Hypothesis Pex : ∃f : set → set , P f
Hypothesis Puniq : ∀f g : set → set , P f → P g → f = g
End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (set → set → set ) → prop
Hypothesis Pex : ∃f : set → set → set , P f
Hypothesis Puniq : ∀f g : set → set → set , P f → P g → f = g
End of Section Descr_iii
Beginning of Section Descr_Vo1
Variable P : Vo 1 → prop
Hypothesis Pex : ∃f : Vo 1 , P f
Hypothesis Puniq : ∀f g : Vo 1 , P f → P g → f = g
End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : set → set
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : set → set → set
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set → (set → set ) → set
Hypothesis Fr : ∀X : set , ∀g h : set → set , (∀x ∈ X , g x = h x ) → F X g = F X h
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set → (set → (set → set ) ) → (set → set )
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set ) , (∀x ∈ X , g x = h x ) → F X g = F X h
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
Variable F : set → (set → (set → set → set ) ) → (set → set → set )
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set → set ) , (∀x ∈ X , g x = h x ) → F X g = F X h
End of Section EpsilonRec_iii
Beginning of Section NatRec
Variable z : set
Variable f : set → set → set
Let F : set → (set → set ) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n ) (g (⋃ n ) ) else z
Axiom. (nat_primrec_r ) We take the following as an axiom:
∀X : set , ∀g h : set → set , (∀x ∈ X , g x = h x ) → F X g = F X h
End of Section NatRec
Beginning of Section NatArith
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_nat .
End of Section NatArith
Notation . We use
+ as an infix operator with priority 450 and which associates to the left corresponding to applying term
setsum .
Beginning of Section pair_setsum
Axiom. (pairI0 ) We take the following as an axiom:
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
Axiom. (pairI1 ) We take the following as an axiom:
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
Axiom. (pairE ) We take the following as an axiom:
∀X Y z, z ∈ pair X Y → (∃x ∈ X , z = pair 0 x ) ∨ (∃y ∈ Y , z = pair 1 y )
Axiom. (pairE0 ) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
Axiom. (pairE1 ) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
Notation . We use
∑ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma .
Axiom. (pair_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀x ∈ X , ∀y ∈ Y x , pair x y ∈ ∑x ∈ X , Y x
Axiom. (proj0_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑x ∈ X , Y x ) → proj0 z ∈ X
Axiom. (pair_Sigma_E1 ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀x y : set , pair x y ∈ (∑x ∈ X , Y x ) → y ∈ Y x
Axiom. (Sigma_E ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑x ∈ X , Y x ) → ∃x ∈ X , ∃y ∈ Y x , z = pair x y
Notation . We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
Let lam : set → (set → set ) → set ≝ Sigma
Notation . When
x is a set, a term
x y is notation for
ap x y .
Notation .
λ x ∈ A ⇒ B is notation for the set
Sigma A (λ x : set ⇒ B ).
Axiom. (lamI ) We take the following as an axiom:
∀X : set , ∀F : set → set , ∀x ∈ X , ∀y ∈ F x , pair x y ∈ λx ∈ X ⇒ F x
Axiom. (lamE ) We take the following as an axiom:
∀X : set , ∀F : set → set , ∀z : set , z ∈ (λx ∈ X ⇒ F x ) → ∃x ∈ X , ∃y ∈ F x , z = pair x y
Axiom. (apI ) We take the following as an axiom:
∀f x y, pair x y ∈ f → y ∈ f x
Axiom. (apE ) We take the following as an axiom:
∀f x y, y ∈ f x → pair x y ∈ f
Axiom. (beta ) We take the following as an axiom:
∀X : set , ∀F : set → set , ∀x : set , x ∈ X → (λx ∈ X ⇒ F x ) x = F x
Axiom. (ap0_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑x ∈ X , Y x ) → (z 0 ) ∈ X
Axiom. (ap1_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑x ∈ X , Y x ) → (z 1 ) ∈ (Y (z 0 ) )
Notation . We use
∏ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi .
Axiom. (PiI ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀f : set , (∀u ∈ f , pair_p u ∧ u 0 ∈ X ) → (∀x ∈ X , f x ∈ Y x ) → f ∈ ∏x ∈ X , Y x
Axiom. (lam_Pi ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀F : set → set , (∀x ∈ X , F x ∈ Y x ) → (λx ∈ X ⇒ F x ) ∈ (∏x ∈ X , Y x )
Axiom. (ap_Pi ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀f : set , ∀x : set , f ∈ (∏x ∈ X , Y x ) → x ∈ X → f x ∈ Y x
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
Axiom. (lamI2 ) We take the following as an axiom:
∀X, ∀F : set → set , ∀x ∈ X , ∀y ∈ F x , (x ,y ) ∈ λx ∈ X ⇒ F x
Beginning of Section Tuples
Variable x0 x1 : set
End of Section Tuples
Axiom. (ReplEq_setprod_ext ) We take the following as an axiom:
∀X Y, ∀F G : set → set → set , (∀x ∈ X , ∀y ∈ Y , F x y = G x y ) → {F (w 0 ) (w 1 ) |w ∈ X ⨯ Y } = {G (w 0 ) (w 1 ) |w ∈ X ⨯ Y }
Axiom. (tuple_2_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀x ∈ X , ∀y ∈ Y x , (x ,y ) ∈ ∑x ∈ X , Y x
End of Section pair_setsum
Notation . We use
∑ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma .
Notation . We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
Notation . We use
∏ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi .
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
Beginning of Section TaggedSets
Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1 }
Notation . We use ' as a postfix operator with priority 100 corresponding to applying term tag .
End of Section TaggedSets
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 .
Beginning of Section TaggedSets2
Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1 }
Notation . We use ' as a postfix operator with priority 100 corresponding to applying term tag .
End of Section TaggedSets2
Axiom. (SNo_ind ) We take the following as an axiom:
∀P : set → prop , (∀L R, SNoCutP L R → (∀x ∈ L , P x ) → (∀y ∈ R , P y ) → P (SNoCut L R ) ) → ∀z, SNo z → P z
Beginning of Section SurrealRecI
Variable F : set → (set → set ) → set
Let G : set → (set → set → set ) → set → set ≝ λalpha g ⇒ If_ii (ordinal alpha ) (λz : set ⇒ if z ∈ SNoS_ (ordsucc alpha ) then F z (λw ⇒ g (SNoLev w ) w ) else default ) (λz : set ⇒ default )
Hypothesis Fr : ∀z, SNo z → ∀g h : set → set , (∀w ∈ SNoS_ (SNoLev z ) , g w = h w ) → F z g = F z h
End of Section SurrealRecI
Beginning of Section SurrealRecII
Variable F : set → (set → (set → set ) ) → (set → set )
Let G : set → (set → set → (set → set ) ) → set → (set → set ) ≝ λalpha g ⇒ If_iii (ordinal alpha ) (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha ) ) (F z (λw ⇒ g (SNoLev w ) w ) ) default ) (λz : set ⇒ default )
Hypothesis Fr : ∀z, SNo z → ∀g h : set → (set → set ) , (∀w ∈ SNoS_ (SNoLev z ) , g w = h w ) → F z g = F z h
End of Section SurrealRecII
Beginning of Section SurrealRec2
Variable F : set → set → (set → set → set ) → set
Let G : set → (set → set → set ) → set → (set → set ) → set ≝ λw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y )
Let H : set → (set → set → set ) → set → set ≝ λw f z ⇒ if SNo z then SNo_rec_i (G w f ) z else Empty
Hypothesis Fr : ∀w, SNo w → ∀z, SNo z → ∀g h : set → set → set , (∀x ∈ SNoS_ (SNoLev w ) , ∀y, SNo y → g x y = h x y ) → (∀y ∈ SNoS_ (SNoLev z ) , g w y = h w y ) → F w z g = F w z h
End of Section SurrealRec2
Axiom. (SNoLev_ind3 ) We take the following as an axiom:
∀P : set → set → set → prop , (∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x ) , P u y z ) → (∀v ∈ SNoS_ (SNoLev y ) , P x v z ) → (∀w ∈ SNoS_ (SNoLev z ) , P x y w ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀v ∈ SNoS_ (SNoLev y ) , P u v z ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀w ∈ SNoS_ (SNoLev z ) , P u y w ) → (∀v ∈ SNoS_ (SNoLev y ) , ∀w ∈ SNoS_ (SNoLev z ) , P x v w ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀v ∈ SNoS_ (SNoLev y ) , ∀w ∈ SNoS_ (SNoLev z ) , P u v w ) → P x y z ) → ∀x y z, SNo x → SNo y → SNo z → P x y z
Beginning of Section SurrealMinus
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 490 and no associativity corresponding to applying term
SNoLe .
End of Section SurrealMinus
Beginning of Section SurrealAdd
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 .
End of Section SurrealAdd
Beginning of Section SurrealMul
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 .
Axiom. (mul_SNo_eq ) We take the following as an axiom:
∀x, SNo x → ∀y, SNo y → x * y = SNoCut ({(w 0 ) * y + x * (w 1 ) + - (w 0 ) * (w 1 ) |w ∈ SNoL x ⨯ SNoL y } ∪ {(z 0 ) * y + x * (z 1 ) + - (z 0 ) * (z 1 ) |z ∈ SNoR x ⨯ SNoR y } ) ({(w 0 ) * y + x * (w 1 ) + - (w 0 ) * (w 1 ) |w ∈ SNoL x ⨯ SNoR y } ∪ {(z 0 ) * y + x * (z 1 ) + - (z 0 ) * (z 1 ) |z ∈ SNoR x ⨯ SNoL y } )
Axiom. (mul_SNo_eq_2 ) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀p : prop , (∀L R, (∀u, u ∈ L → (∀q : prop , (∀w0 ∈ SNoL x , ∀w1 ∈ SNoL y , u = w0 * y + x * w1 + - w0 * w1 → q ) → (∀z0 ∈ SNoR x , ∀z1 ∈ SNoR y , u = z0 * y + x * z1 + - z0 * z1 → q ) → q ) ) → (∀w0 ∈ SNoL x , ∀w1 ∈ SNoL y , w0 * y + x * w1 + - w0 * w1 ∈ L ) → (∀z0 ∈ SNoR x , ∀z1 ∈ SNoR y , z0 * y + x * z1 + - z0 * z1 ∈ L ) → (∀u, u ∈ R → (∀q : prop , (∀w0 ∈ SNoL x , ∀z1 ∈ SNoR y , u = w0 * y + x * z1 + - w0 * z1 → q ) → (∀z0 ∈ SNoR x , ∀w1 ∈ SNoL y , u = z0 * y + x * w1 + - z0 * w1 → q ) → q ) ) → (∀w0 ∈ SNoL x , ∀z1 ∈ SNoR y , w0 * y + x * z1 + - w0 * z1 ∈ R ) → (∀z0 ∈ SNoR x , ∀w1 ∈ SNoL y , z0 * y + x * w1 + - z0 * w1 ∈ R ) → x * y = SNoCut L R → p ) → p
Axiom. (mul_SNo_prop_1 ) We take the following as an axiom:
∀x, SNo x → ∀y, SNo y → ∀p : prop , (SNo (x * y ) → (∀u ∈ SNoL x , ∀v ∈ SNoL y , u * y + x * v < x * y + u * v ) → (∀u ∈ SNoR x , ∀v ∈ SNoR y , u * y + x * v < x * y + u * v ) → (∀u ∈ SNoL x , ∀v ∈ SNoR y , x * y + u * v < u * y + x * v ) → (∀u ∈ SNoR x , ∀v ∈ SNoL y , x * y + u * v < u * y + x * v ) → p ) → p
Axiom. (mul_SNo_eq_3 ) We take the following as an axiom:
∀x y, SNo x → SNo y → ∀p : prop , (∀L R, SNoCutP L R → (∀u, u ∈ L → (∀q : prop , (∀w0 ∈ SNoL x , ∀w1 ∈ SNoL y , u = w0 * y + x * w1 + - w0 * w1 → q ) → (∀z0 ∈ SNoR x , ∀z1 ∈ SNoR y , u = z0 * y + x * z1 + - z0 * z1 → q ) → q ) ) → (∀w0 ∈ SNoL x , ∀w1 ∈ SNoL y , w0 * y + x * w1 + - w0 * w1 ∈ L ) → (∀z0 ∈ SNoR x , ∀z1 ∈ SNoR y , z0 * y + x * z1 + - z0 * z1 ∈ L ) → (∀u, u ∈ R → (∀q : prop , (∀w0 ∈ SNoL x , ∀z1 ∈ SNoR y , u = w0 * y + x * z1 + - w0 * z1 → q ) → (∀z0 ∈ SNoR x , ∀w1 ∈ SNoL y , u = z0 * y + x * w1 + - z0 * w1 → q ) → q ) ) → (∀w0 ∈ SNoL x , ∀z1 ∈ SNoR y , w0 * y + x * z1 + - w0 * z1 ∈ R ) → (∀z0 ∈ SNoR x , ∀w1 ∈ SNoL y , z0 * y + x * w1 + - z0 * w1 ∈ R ) → x * y = SNoCut L R → p ) → p
Axiom. (mul_SNo_Subq_lem ) We take the following as an axiom:
∀x y X Y Z W, ∀U U', (∀u, u ∈ U → (∀q : prop , (∀w0 ∈ X , ∀w1 ∈ Y , u = w0 * y + x * w1 + - w0 * w1 → q ) → (∀z0 ∈ Z , ∀z1 ∈ W , u = z0 * y + x * z1 + - z0 * z1 → q ) → q ) ) → (∀w0 ∈ X , ∀w1 ∈ Y , w0 * y + x * w1 + - w0 * w1 ∈ U' ) → (∀w0 ∈ Z , ∀w1 ∈ W , w0 * y + x * w1 + - w0 * w1 ∈ U' ) → U ⊆ U'
Beginning of Section mul_SNo_assoc_lems
Variable M : set → set → set
Notation . We use * as an infix operator with priority 355 and which associates to the right corresponding to applying term M .
Hypothesis SNo_M : ∀x y, SNo x → SNo y → SNo (x * y )
Hypothesis DL : ∀x y z, SNo x → SNo y → SNo z → x * (y + z ) = x * y + x * z
Hypothesis DR : ∀x y z, SNo x → SNo y → SNo z → (x + y ) * z = x * z + y * z
Hypothesis IL : ∀x y, SNo x → SNo y → ∀u ∈ SNoL (x * y ) , ∀p : prop , (∀v ∈ SNoL x , ∀w ∈ SNoL y , u + v * w ≤ v * y + x * w → p ) → (∀v ∈ SNoR x , ∀w ∈ SNoR y , u + v * w ≤ v * y + x * w → p ) → p
Hypothesis IR : ∀x y, SNo x → SNo y → ∀u ∈ SNoR (x * y ) , ∀p : prop , (∀v ∈ SNoL x , ∀w ∈ SNoR y , v * y + x * w ≤ u + v * w → p ) → (∀v ∈ SNoR x , ∀w ∈ SNoL y , v * y + x * w ≤ u + v * w → p ) → p
Hypothesis M_Lt : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u < x → v < y → u * y + x * v < x * y + u * v
Hypothesis M_Le : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u ≤ x → v ≤ y → u * y + x * v ≤ x * y + u * v
Axiom. (mul_SNo_assoc_lem1 ) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x ) , u * (y * z ) = (u * y ) * z ) → (∀v ∈ SNoS_ (SNoLev y ) , x * (v * z ) = (x * v ) * z ) → (∀w ∈ SNoS_ (SNoLev z ) , x * (y * w ) = (x * y ) * w ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀v ∈ SNoS_ (SNoLev y ) , u * (v * z ) = (u * v ) * z ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀w ∈ SNoS_ (SNoLev z ) , u * (y * w ) = (u * y ) * w ) → (∀v ∈ SNoS_ (SNoLev y ) , ∀w ∈ SNoS_ (SNoLev z ) , x * (v * w ) = (x * v ) * w ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀v ∈ SNoS_ (SNoLev y ) , ∀w ∈ SNoS_ (SNoLev z ) , u * (v * w ) = (u * v ) * w ) → ∀L, (∀u ∈ L , ∀q : prop , (∀v ∈ SNoL x , ∀w ∈ SNoL (y * z ) , u = v * (y * z ) + x * w + - v * w → q ) → (∀v ∈ SNoR x , ∀w ∈ SNoR (y * z ) , u = v * (y * z ) + x * w + - v * w → q ) → q ) → ∀u ∈ L , u < (x * y ) * z
Axiom. (mul_SNo_assoc_lem2 ) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x ) , u * (y * z ) = (u * y ) * z ) → (∀v ∈ SNoS_ (SNoLev y ) , x * (v * z ) = (x * v ) * z ) → (∀w ∈ SNoS_ (SNoLev z ) , x * (y * w ) = (x * y ) * w ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀v ∈ SNoS_ (SNoLev y ) , u * (v * z ) = (u * v ) * z ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀w ∈ SNoS_ (SNoLev z ) , u * (y * w ) = (u * y ) * w ) → (∀v ∈ SNoS_ (SNoLev y ) , ∀w ∈ SNoS_ (SNoLev z ) , x * (v * w ) = (x * v ) * w ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀v ∈ SNoS_ (SNoLev y ) , ∀w ∈ SNoS_ (SNoLev z ) , u * (v * w ) = (u * v ) * w ) → ∀R, (∀u ∈ R , ∀q : prop , (∀v ∈ SNoL x , ∀w ∈ SNoR (y * z ) , u = v * (y * z ) + x * w + - v * w → q ) → (∀v ∈ SNoR x , ∀w ∈ SNoL (y * z ) , u = v * (y * z ) + x * w + - v * w → q ) → q ) → ∀u ∈ R , (x * y ) * z < u
End of Section mul_SNo_assoc_lems
Axiom. (SNo_foil ) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + y ) * (z + w ) = x * z + x * w + y * z + y * w
Axiom. (SNo_foil_mm ) We take the following as an axiom:
∀x y z w, SNo x → SNo y → SNo z → SNo w → (x + - y ) * (z + - w ) = x * z + - x * w + - y * z + y * w
End of Section SurrealMul
Beginning of Section SurrealExp
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 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
End of Section SurrealExp
Beginning of Section Int
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 .
End of Section Int
Beginning of Section SurrealAbs
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 .
End of Section SurrealAbs
Beginning of Section SNoMaxMin
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 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
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 .
End of Section SNoMaxMin
Beginning of Section DiadicRationals
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 .
End of Section DiadicRationals
Part 8
Beginning of Section Reals
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 .
Proof: Let x be given.
Assume Hx .
Assume Hx1 Hx2 Hx3 Hx4 .
Let k be given.
Assume Hk .
We will
prove ∃q ∈ SNoS_ ω , q < x ∧ x < q + eps_ k .
We use
x + - eps_ (ordsucc k ) to
witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
∎
Proof: Let x be given.
Assume Hx1 Hx2 .
Assume Hx1a Hx1b Hx1c Hx1d .
Let z be given.
Assume Hz5 : x < z .
An exact proof term for the current goal is Hz1 .
We prove the intermediate
claim Lz2 :
SNo (SNoLev z ) .
An exact proof term for the current goal is Lz1 .
We use
(SNoLev z ) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz8 .
An exact proof term for the current goal is Hx1c .
An exact proof term for the current goal is Lx1 .
We use
(ordsucc (SNoLev x ) ) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3 .
rewrite the current goal using H2 (from right to left) at position 2.
An exact proof term for the current goal is H1 .
∎
Proof: Let x be given.
Assume Hx1 Hx2 .
Assume Hx1a Hx1b Hx1c Hx1d .
We prove the intermediate
claim Lx2 :
- x < ω .
An exact proof term for the current goal is Hx2 .
Let N be given.
Assume HN .
Apply HN to the current goal.
Assume HN2 : - x < N .
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1 .
We will prove - N < x .
We will prove - x < N .
An exact proof term for the current goal is HN2 .
∎
Proof: Let x be given.
Assume Hx1 Hx2 Hx3 .
Assume Hx1a Hx1b Hx1c Hx1d .
Apply dneg to the current goal.
We prove the intermediate
claim L1 :
x ∉ SNoS_ ω .
Apply HC to the current goal.
We prove the intermediate
claim L2 :
∀k, nat_p k → ∃q ∈ SNoS_ ω , q < x ∧ x < q + eps_ k .
We will
prove ∃q ∈ SNoS_ ω , q < x ∧ x < q + eps_ 0 .
rewrite the current goal using
eps_0_1 (from left to right).
We will
prove ∃q ∈ SNoS_ ω , q < x ∧ x < q + 1 .
We prove the intermediate
claim L1a :
∀N, nat_p N → - N < x → x < N → ∃q ∈ SNoS_ ω , q < x ∧ x < q + 1 .
rewrite the current goal using
minus_SNo_0 (from left to right).
Assume H1 : 0 < x .
Assume H2 : x < 0 .
An
exact proof term for the current goal is
SNoLt_tra x 0 x Hx1c SNo_0 Hx1c H2 H1 .
Let N be given.
Assume HN .
We will
prove ∃q ∈ SNoS_ ω , q < x ∧ x < q + 1 .
We prove the intermediate
claim LN1 :
SNo N .
An
exact proof term for the current goal is
nat_p_SNo N HN .
We prove the intermediate
claim LN2 :
SNo (- N ) .
We prove the intermediate
claim LN3 :
N ∈ SNoS_ ω .
An
exact proof term for the current goal is
nat_p_omega N HN .
Assume H3 : x < N .
Assume H4 : x < - N .
We use
(- ordsucc N ) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN .
Apply andI to the current goal.
An exact proof term for the current goal is H1 .
We will prove x < - (N + 1 ) + 1 .
We will prove x < (- N + - 1 ) + 1 .
We will prove x < - N .
An exact proof term for the current goal is H4 .
Assume H4 : x = - N .
Apply L1 to the current goal.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is LN3 .
Assume H4 : - N < x .
An exact proof term for the current goal is IHN H4 H3 .
Assume H3 : x = N .
Apply L1 to the current goal.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is LN3 .
Assume H3 : N < x .
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is LN3 .
Apply andI to the current goal.
We will prove N < x .
An exact proof term for the current goal is H3 .
We will prove x < N + 1 .
An exact proof term for the current goal is H2 .
Let N be given.
Assume HN .
Apply HN to the current goal.
Assume HN2 : x < N .
Let N' be given.
Assume HN' .
Apply HN' to the current goal.
Assume HN'2 : - N' < x .
Assume H1 : N < N' .
Apply L1a N' (omega_nat_p N' HN'1 ) HN'2 to the current goal.
We will prove x < N' .
Assume H1 : N = N' .
Apply L1a N' (omega_nat_p N' HN'1 ) HN'2 to the current goal.
We will prove x < N' .
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is HN2 .
Assume H1 : N' < N .
We will prove - N < x .
We will prove - N < - N' .
An exact proof term for the current goal is H1 .
We will prove - N' < x .
An exact proof term for the current goal is HN'2 .
We will prove x < N .
An exact proof term for the current goal is HN2 .
Let k be given.
Assume Hk .
Assume IHk .
Apply IHk to the current goal.
Let q be given.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume Hq2 : q < x .
Assume Hq1a Hq1b Hq1c Hq1d .
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq1 .
Apply andI to the current goal.
An exact proof term for the current goal is Hq2 .
An exact proof term for the current goal is H1 .
Apply L1 to the current goal.
rewrite the current goal using H1 (from left to right).
We use
(q + eps_ (ordsucc k ) ) to
witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H1 .
We will
prove x < q + eps_ k .
An exact proof term for the current goal is Hq3 .
Apply HC to the current goal.
Let k be given.
Assume Hk .
An
exact proof term for the current goal is
L2 k (omega_nat_p k Hk ) .
∎
Proof: Let x be given.
Assume Hx H1 H2 H3 .
Apply SepI to the current goal.
An exact proof term for the current goal is Hx .
Apply and3I to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H3 .
∎
Proof: Let x be given.
Assume Hx .
Let p be given.
Assume Hp .
Assume H1 H2 .
Apply H2 to the current goal.
Assume H2 .
Apply H2 to the current goal.
Assume H4 .
Assume H1a H1b H1c H1d .
We prove the intermediate
claim L1 :
x < ω .
We prove the intermediate
claim L1a :
x ≤ ω .
An exact proof term for the current goal is H1a .
Assume H .
An exact proof term for the current goal is H .
An exact proof term for the current goal is H2 H .
We prove the intermediate
claim L2 :
- ω < x .
We prove the intermediate
claim L2a :
- ω ≤ x .
An exact proof term for the current goal is H1a .
Assume H .
An exact proof term for the current goal is H .
Apply H3 to the current goal.
Use symmetry.
An exact proof term for the current goal is H .
We prove the intermediate
claim L3 :
∀k ∈ ω , ∃q ∈ SNoS_ ω , q < x ∧ x < q + eps_ k .
An exact proof term for the current goal is Hp H1c H1a H1 L2 L1 H4 L3 .
∎
Proof: Let x be given.
Assume Hx .
Apply real_E x Hx to the current goal.
Assume Hx1 _ _ _ _ _ _ .
An exact proof term for the current goal is Hx1 .
∎
Proof: Let x be given.
Assume Hx .
Apply real_E x Hx to the current goal.
Assume _ _ _ _ _ Hx6 _ .
An exact proof term for the current goal is Hx6 .
∎
Proof: Let x be given.
Assume Hx1 Hx2 Hx3 Hx4 .
Apply real_I to the current goal.
An exact proof term for the current goal is Hx .
rewrite the current goal using H1 (from left to right) at position 2.
An exact proof term for the current goal is Hx1 .
rewrite the current goal using H1 (from left to right) at position 2.
An exact proof term for the current goal is Hx1 .
Let q be given.
Assume Hq1 Hq2 Hq3 Hq4 .
We will prove q = x .
Assume Hqx : q < x .
We prove the intermediate claim L1 : 0 < x + - q .
An exact proof term for the current goal is Hqx .
We prove the intermediate
claim L2 :
x + - q ∈ SNoS_ ω .
We prove the intermediate
claim L3 :
abs_SNo (q + - x ) = x + - q .
An
exact proof term for the current goal is
pos_abs_SNo (x + - q ) L1 .
rewrite the current goal using L3 (from right to left) at position 1.
An
exact proof term for the current goal is
H1 (SNoLev (x + - q ) ) H2 .
An exact proof term for the current goal is H5 .
An exact proof term for the current goal is L1 .
Assume Hqx : q = x .
An exact proof term for the current goal is Hqx .
Assume Hxq : x < q .
We prove the intermediate claim L4 : 0 < q + - x .
An exact proof term for the current goal is Hxq .
We prove the intermediate
claim L5 :
q + - x ∈ SNoS_ ω .
We prove the intermediate
claim L6 :
abs_SNo (q + - x ) = q + - x .
An
exact proof term for the current goal is
pos_abs_SNo (q + - x ) L4 .
rewrite the current goal using L6 (from right to left) at position 1.
An
exact proof term for the current goal is
H1 (SNoLev (q + - x ) ) H2 .
An exact proof term for the current goal is H5 .
An exact proof term for the current goal is L4 .
∎
Proof: Let x be given.
Assume Hx .
Let w be given.
Assume Hw1 Hw2 .
Apply real_E x Hx to the current goal.
Assume _ _ _ _ _ .
We prove the intermediate
claim L1 :
SNoLev w ∈ ω .
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hw2 .
An exact proof term for the current goal is Hw1 .
∎
Proof: Let x be given.
Assume Hx H1 .
Let q be given.
We will prove q = - x .
Assume Hq1a Hq1b Hq1c Hq1d .
rewrite the current goal using
minus_SNo_invol q Hq1c (from right to left).
We will prove - - q = - x .
Use f_equal.
We will prove - q = x .
Let k be given.
Assume Hk .
rewrite the current goal using
minus_SNo_invol q Hq1c (from left to right).
rewrite the current goal using
add_SNo_com x q Hx Hq1c (from left to right).
An exact proof term for the current goal is Hq2 k Hk .
∎
Proof: Let x be given.
Assume Hx H1 .
Let k be given.
Assume Hk .
Apply H1 k Hk to the current goal.
Let q be given.
Assume Hq .
Apply Hq to the current goal.
Assume Hq .
Apply Hq to the current goal.
Assume Hq2 : q < x .
Assume Hq1a Hq1b Hq1c Hq1d .
We prove the intermediate
claim Lqk :
SNo (q + eps_ k ) .
We use
(- (q + eps_ k ) ) to
witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We will
prove - (q + eps_ k ) < - x .
We will
prove x < q + eps_ k .
An exact proof term for the current goal is Hq3 .
We will
prove - x < - (q + eps_ k ) + eps_ k .
We will
prove - x < (- q + - eps_ k ) + eps_ k .
We will prove - x < - q .
We will prove q < x .
An exact proof term for the current goal is Hq2 .
∎
Proof: Let x be given.
Assume Hx Hx0 Hx2 Hx3 .
Let k be given.
Assume Hk .
Let p be given.
Assume Hp .
Apply Hx3 k Hk to the current goal.
Let q be given.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume Hq2 : q < x .
Assume Hq1a Hq1b Hq1c Hq1d .
Assume H1 : 0 < q .
An exact proof term for the current goal is Hp q Hq1 H1 Hq2 Hq3 .
Assume H1 : q ≤ 0 .
Apply xm (∀k' ∈ ω , x < eps_ k' ) to the current goal.
We prove the intermediate claim L1 : 0 = x .
Let k' be given.
rewrite the current goal using
abs_SNo_minus x Hx (from left to right).
rewrite the current goal using
pos_abs_SNo x Hx0 (from left to right).
An exact proof term for the current goal is H2 k' Hk' .
We will prove x < x .
rewrite the current goal using L1 (from right to left) at position 1.
An exact proof term for the current goal is Hx0 .
Apply dneg to the current goal.
Assume H3 : ¬ p .
Apply H2 to the current goal.
Let k' be given.
An exact proof term for the current goal is H4 .
We prove the intermediate
claim Lek' :
SNo (eps_ k' ) .
An exact proof term for the current goal is Hk' .
An exact proof term for the current goal is Hk' .
We prove the intermediate
claim LeSk'pos :
0 < eps_ (ordsucc k' ) .
An exact proof term for the current goal is Hk' .
Apply H3 to the current goal.
An exact proof term for the current goal is Hk' .
An exact proof term for the current goal is LeSk'pos .
We will
prove eps_ k' ≤ x .
An exact proof term for the current goal is H4 .
We prove the intermediate
claim L2 :
q < eps_ (ordsucc k' ) .
We will prove q ≤ 0 .
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is LeSk'pos .
We will
prove x < q + eps_ k .
An exact proof term for the current goal is Hq3 .
An exact proof term for the current goal is L2 .
∎
Proof: Let x be given.
Assume Hx .
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 .
Apply real_I to the current goal.
We will prove x < x .
rewrite the current goal using
minus_SNo_invol x Hx1 (from right to left) at position 1.
We will prove - - x < x .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hx4 .
We will prove x < x .
rewrite the current goal using
minus_SNo_invol x Hx1 (from right to left) at position 2.
We will prove x < - - x .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hx5 .
∎
Proof: Let x be given.
Assume H1 H2 H3 .
Set f to be the term
λn ∈ ω ⇒ f' n .
We prove the intermediate
claim Lf'0 :
f' 0 = Eps_i (λq ⇒ q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ 0 ) .
We prove the intermediate
claim Lf'0b :
f' 0 ∈ SNoS_ ω ∧ f' 0 < x ∧ x < f' 0 + eps_ 0 .
rewrite the current goal using Lf'0 (from left to right).
We will
prove ∃q, q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ 0 .
Let q be given.
Assume Hq .
Apply Hq to the current goal.
Assume Hq1 Hq .
Apply Hq to the current goal.
Assume Hq2 Hq3 .
We use q to witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is Hq1 .
An exact proof term for the current goal is Hq2 .
An exact proof term for the current goal is Hq3 .
We prove the intermediate
claim L1 :
∀n, nat_p n → f' n ∈ SNoS_ ω ∧ f' n < x ∧ x < f' n + eps_ n ∧ ∀i ∈ n , SNo (f i ) → f i < f' n .
We will
prove f' 0 ∈ SNoS_ ω ∧ f' 0 < x ∧ x < f' 0 + eps_ 0 ∧ ∀i ∈ 0 , SNo (f i ) → f i < f' 0 .
Apply Lf'0b to the current goal.
Assume H H6 .
Apply H to the current goal.
Assume H4 H5 .
Apply and4I to the current goal.
An exact proof term for the current goal is H4 .
An exact proof term for the current goal is H5 .
An exact proof term for the current goal is H6 .
Let i be given.
Assume Hi .
An
exact proof term for the current goal is
EmptyE i Hi .
Let n be given.
Assume Hn .
Apply IHn to the current goal.
Assume IHn123 IHn4 .
Apply IHn123 to the current goal.
Assume IHn12 IHn3 .
Apply IHn12 to the current goal.
Assume IHn1 IHn2 .
Assume _ _ .
Assume _ .
We prove the intermediate
claim L1b :
∃q, q ∈ SNoS_ ω ∧ q < x ∧ x < q + eps_ (ordsucc n ) ∧ f' n < q .
Let q be given.
Assume Hq .
Apply Hq to the current goal.
Assume Hq1 Hq .
Apply Hq to the current goal.
Assume Hq2 Hq3 .
Assume Hq1a Hq1b Hq1c Hq1d .
Apply SNoLtLe_or (f' n ) q IHn1c Hq1c to the current goal.
Assume H4 : f' n < q .
We use q to witness the existential quantifier.
Apply and4I to the current goal.
An exact proof term for the current goal is Hq1 .
An exact proof term for the current goal is Hq2 .
An exact proof term for the current goal is Hq3 .
An exact proof term for the current goal is H4 .
Assume H4 : q ≤ f' n .
We prove the intermediate
claim L1ba :
SNo (- f' n ) .
An
exact proof term for the current goal is
SNo_minus_SNo (f' n ) IHn1c .
We prove the intermediate
claim L1bb :
SNo (x + - f' n ) .
An
exact proof term for the current goal is
SNo_add_SNo x (- f' n ) H1 L1ba .
Apply xm (∃k ∈ ω , eps_ k ≤ x + - f' n ) to the current goal.
Assume H5 .
Apply H5 to the current goal.
Let k be given.
Assume H5 .
Apply H5 to the current goal.
We use
(f' n + eps_ (ordsucc k ) ) to
witness the existential quantifier.
We prove the intermediate
claim Lk1 :
ordsucc k ∈ ω .
Assume _ _ .
Assume _ .
Apply and4I to the current goal.
An exact proof term for the current goal is Lk3 .
An exact proof term for the current goal is H6 .
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is Lk1 .
We will
prove f' n + eps_ k ≤ x .
We will
prove f' n + eps_ k ≤ f' n + (- f' n + x ) .
rewrite the current goal using
add_SNo_com (- f' n ) x L1ba H1 (from left to right).
We will
prove f' n + eps_ k ≤ f' n + (x + - f' n ) .
An
exact proof term for the current goal is
add_SNo_Le2 (f' n ) (eps_ k ) (x + - f' n ) IHn1c (SNo_eps_ k Hk1 ) L1bb Hk2 .
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is Hq3 .
We will prove x < x .
We prove the intermediate claim L1bd : 0 < x + - f' n .
We will prove 0 + f' n < (x + - f' n ) + f' n .
rewrite the current goal using
add_SNo_0L (f' n ) IHn1c (from left to right).
rewrite the current goal using
add_SNo_minus_R2' x (f' n ) H1 IHn1c (from left to right).
We will prove f' n < x .
An exact proof term for the current goal is IHn2 .
We prove the intermediate claim L1be : f' n = x .
Apply H2 (f' n ) IHn1 to the current goal.
Let k be given.
Assume Hk .
rewrite the current goal using
abs_SNo_dist_swap (f' n ) x IHn1c H1 (from left to right).
rewrite the current goal using
pos_abs_SNo (x + - f' n ) L1bd (from left to right).
An exact proof term for the current goal is H6 .
Apply H5 to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk .
An exact proof term for the current goal is H6 .
rewrite the current goal using L1be (from right to left) at position 1.
An exact proof term for the current goal is IHn2 .
rewrite the current goal using Lf'S n Hn (from left to right).
Apply L1c to the current goal.
Assume H H7 .
Apply H to the current goal.
Assume H H6 .
Apply H to the current goal.
Assume H4 H5 .
Apply and4I to the current goal.
An exact proof term for the current goal is H4 .
An exact proof term for the current goal is H5 .
An exact proof term for the current goal is H6 .
Let i be given.
Apply ordsuccE n i Hi to the current goal.
Assume H8 : i ∈ n .
We will
prove f i < f' (ordsucc n ) .
An exact proof term for the current goal is Hfi .
An exact proof term for the current goal is IHn1c .
Assume _ _ H9 _ .
An exact proof term for the current goal is H9 .
Apply IHn to the current goal.
Assume _ .
An exact proof term for the current goal is IHn4 i H8 Hfi .
An exact proof term for the current goal is H7 .
Assume H8 : i = n .
rewrite the current goal using H8 (from left to right).
We will
prove f n < f' (ordsucc n ) .
rewrite the current goal using
beta ω f' n (nat_p_omega n Hn ) (from left to right).
An exact proof term for the current goal is H7 .
We prove the intermediate
claim L2 :
∀n ∈ ω , f' n ∈ SNoS_ ω ∧ f n < x ∧ x < f n + eps_ n ∧ ∀i ∈ n , SNo (f i ) → f i < f n .
Let n be given.
Assume Hn .
An
exact proof term for the current goal is
beta ω f' n Hn (λu v ⇒ f' n ∈ SNoS_ ω ∧ v < x ∧ x < v + eps_ n ∧ ∀i ∈ n , SNo (f i ) → f i < v ) (L1 n (omega_nat_p n Hn ) ) .
We use f to witness the existential quantifier.
Apply andI to the current goal.
We will
prove (λn ∈ ω ⇒ f' n ) ∈ ∏n ∈ ω , SNoS_ ω .
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn .
Apply L2 n Hn to the current goal.
Assume H _ .
Apply H to the current goal.
Assume H _ .
Apply H to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
Let n be given.
Assume Hn .
Apply L2 n Hn to the current goal.
Assume H H7 .
Apply H to the current goal.
Assume H H6 .
Apply H to the current goal.
Assume H4 H5 .
Apply and3I to the current goal.
An exact proof term for the current goal is H5 .
An exact proof term for the current goal is H6 .
Let i be given.
Assume Hi : i ∈ n .
Apply H7 i Hi to the current goal.
We prove the intermediate
claim Li :
i ∈ ω .
rewrite the current goal using
beta ω f' i Li (from left to right).
We will
prove SNo (f' i ) .
Apply L2 i Li to the current goal.
Assume H _ .
Apply H to the current goal.
Assume H _ .
Apply H to the current goal.
Assume _ .
Assume _ _ H9 _ .
We will
prove SNo (f' i ) .
An exact proof term for the current goal is H9 .
∎
Proof: Let x be given.
Assume H1 H2 H3 .
We prove the intermediate
claim L1 :
SNo (- x ) .
Let f be given.
Assume Hf .
Apply Hf to the current goal.
We prove the intermediate
claim Lf :
∀n ∈ ω , SNo (f n ) .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H .
Set g to be the term
λn ∈ ω ⇒ - f n .
We use g to witness the existential quantifier.
Apply andI to the current goal.
We will
prove (λn ∈ ω ⇒ - f n ) ∈ ∏_ ∈ ω , SNoS_ ω .
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn .
We will
prove - f n ∈ SNoS_ ω .
An
exact proof term for the current goal is
ap_Pi ω (λ_ ⇒ SNoS_ ω ) f n Hf1 Hn .
Let n be given.
Assume Hn .
We will
prove g n + - eps_ n < x ∧ x < g n ∧ ∀i ∈ n , g n < g i .
We prove the intermediate
claim L1 :
- f n + - eps_ n < x ∧ x < - f n ∧ ∀i ∈ n , - f n < g i .
Apply Hf2 n Hn to the current goal.
Assume H .
Apply H to the current goal.
Assume Hf2a : f n < - x .
Assume Hf2c : ∀i ∈ n , f i < f n .
Apply and3I to the current goal.
We will
prove - f n + - eps_ n < x .
We will
prove - (f n + eps_ n ) < x .
We will
prove - x < f n + eps_ n .
An exact proof term for the current goal is Hf2b .
We will prove x < - f n .
We will prove f n < - x .
An exact proof term for the current goal is Hf2a .
Let i be given.
Assume Hi .
We prove the intermediate
claim Li :
i ∈ ω .
rewrite the current goal using
beta ω (λn ⇒ - f n ) i Li (from left to right).
We will prove - f n < - f i .
An exact proof term for the current goal is Hf2c i Hi .
We prove the intermediate claim L2 : g n = - f n .
An
exact proof term for the current goal is
beta ω (λn ⇒ - f n ) n Hn .
An
exact proof term for the current goal is
L2 (λu v ⇒ v + - eps_ n < x ∧ x < v ∧ ∀i ∈ n , v < g i ) L1 .
∎
Proof: Let lambda be given.
Assume Hl1 Hl2 .
Let L be given.
Assume HL .
Let R be given.
Assume HR HLR .
We prove the intermediate
claim L1 :
∀x ∈ L , SNoLev x ∈ lambda .
Let x be given.
Assume Hx .
Apply SNoS_E2 lambda Hl1 x (HL x Hx ) to the current goal.
Assume H _ _ _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim L2 :
∀y ∈ R , SNoLev y ∈ lambda .
Let y be given.
Assume Hy .
Apply SNoS_E2 lambda Hl1 y (HR y Hy ) to the current goal.
Assume H _ _ _ .
An exact proof term for the current goal is H .
Let x be given.
Assume Hx .
Apply SNoS_E2 lambda Hl1 x (HL x Hx ) to the current goal.
Assume _ H _ _ .
An exact proof term for the current goal is H .
Let y be given.
Assume Hy .
Apply SNoS_E2 lambda Hl1 y (HR y Hy ) to the current goal.
Assume _ H _ _ .
An exact proof term for the current goal is H .
An exact proof term for the current goal is Hl1 .
An exact proof term for the current goal is L4 .
Assume H1 .
An exact proof term for the current goal is H1 .
Let x be given.
Assume Hx : x ∈ L .
Apply Hl2 to the current goal.
An exact proof term for the current goal is L1 x Hx .
Let y be given.
Assume Hy : y ∈ R .
Apply Hl2 to the current goal.
An exact proof term for the current goal is L2 y Hy .
Assume _ _ _ .
An
exact proof term for the current goal is
L5 (SNoLev (SNoCut L R ) ) H2 .
∎
Proof: Let f be given.
Assume Hf1 .
Let g be given.
Assume Hg1 Hfg .
Let p be given.
Assume Hp .
Set L to be the term
{f n |n ∈ ω } .
Set R to be the term
{g n |n ∈ ω } .
Set x to be the term
SNoCut L R .
We prove the intermediate
claim Lf :
∀n ∈ ω , SNo (f n ) .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lg :
∀n ∈ ω , SNo (g n ) .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim L1 :
SNoCutP L R .
We will
prove (∀w ∈ L , SNo w ) ∧ (∀z ∈ R , SNo z ) ∧ (∀w ∈ L , ∀z ∈ R , w < z ) .
Apply and3I to the current goal.
Let w be given.
Assume Hw : w ∈ L .
Let n be given.
Assume Hn .
Assume Hwn : w = f n .
rewrite the current goal using Hwn (from left to right).
An exact proof term for the current goal is Lf n Hn .
Let z be given.
Assume Hz : z ∈ R .
Let m be given.
Assume Hm .
Assume Hzm : z = g m .
rewrite the current goal using Hzm (from left to right).
An exact proof term for the current goal is Lg m Hm .
Let w be given.
Assume Hw : w ∈ L .
Let z be given.
Assume Hz : z ∈ R .
Let n be given.
Assume Hn .
Assume Hwn : w = f n .
rewrite the current goal using Hwn (from left to right).
Let m be given.
Assume Hm .
Assume Hzm : z = g m .
rewrite the current goal using Hzm (from left to right).
We will prove f n < g m .
An exact proof term for the current goal is Hfg n Hn m Hm .
Assume HLR3 : ∀w ∈ L , w < x .
Assume HLR4 : ∀y ∈ R , x < y .
We prove the intermediate
claim L2 :
L ⊆ SNoS_ ω .
Let w be given.
Assume Hw .
Let n be given.
Assume Hn .
Assume Hwn : w = f n .
rewrite the current goal using Hwn (from left to right).
An
exact proof term for the current goal is
ap_Pi ω (λ_ ⇒ SNoS_ ω ) f n Hf1 Hn .
We prove the intermediate
claim L3 :
R ⊆ SNoS_ ω .
Let z be given.
Assume Hz : z ∈ R .
Let m be given.
Assume Hm .
Assume Hzm : z = g m .
rewrite the current goal using Hzm (from left to right).
An
exact proof term for the current goal is
(ap_Pi ω (λ_ ⇒ SNoS_ ω ) g m Hg1 Hm ) .
An exact proof term for the current goal is L4 .
An exact proof term for the current goal is HLR1 .
Apply Hp L1 HLR1 L4 L5 to the current goal.
Let n be given.
Assume Hn .
We will prove f n < x .
Apply HLR3 to the current goal.
An
exact proof term for the current goal is
ReplI ω (λn ⇒ f n ) n Hn .
Let n be given.
Assume Hn .
We will prove x < g n .
Apply HLR4 to the current goal.
An
exact proof term for the current goal is
ReplI ω (λn ⇒ g n ) n Hn .
∎
Proof: Let x be given.
Assume Hx .
Let f be given.
Assume Hf1 .
Let g be given.
Assume Hg1 Hf2 Hf3 Hf4 Hg3 Hg4 .
Set L to be the term
{f n |n ∈ ω } .
Set R to be the term
{g n |n ∈ ω } .
We prove the intermediate
claim Lmx :
SNo (- x ) .
We prove the intermediate
claim Lf :
∀n ∈ ω , SNo (f n ) .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lg :
∀n ∈ ω , SNo (g n ) .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lfg :
∀n m ∈ ω , f n < g m .
Let n be given.
Assume Hn .
Let m be given.
Assume Hm .
Apply SNoLt_tra (f n ) x (g m ) (Lf n Hn ) Hx (Lg m Hm ) to the current goal.
An exact proof term for the current goal is Hf2 n Hn .
An exact proof term for the current goal is Hg3 m Hm .
rewrite the current goal using Hxfg (from right to left).
rewrite the current goal using Hxfg (from right to left).
rewrite the current goal using Hxfg (from right to left).
rewrite the current goal using Hxfg (from right to left).
rewrite the current goal using Hxfg (from right to left).
Assume _ _ _ _ .
An
exact proof term for the current goal is
SNoLev_ x Hx .
Apply real_I to the current goal.
An exact proof term for the current goal is H4 .
We prove the intermediate claim Lbd1 : x < g 0 .
Assume _ _ _ .
Assume _ _ .
We will prove x < x .
Apply SNoLt_tra x (g 0 ) x Hx Hg0a Hx Lbd1 to the current goal.
We will prove g 0 < x .
rewrite the current goal using H9 (from left to right).
An exact proof term for the current goal is Hg0b .
We prove the intermediate claim Lbd2 : f 0 < x .
Assume _ _ .
Assume _ _ _ .
We will prove x < x .
Apply SNoLt_tra x (f 0 ) x Hx Hf0a Hx to the current goal.
We will prove x < f 0 .
rewrite the current goal using H9 (from left to right).
An exact proof term for the current goal is Hf0b .
We will prove f 0 < x .
An exact proof term for the current goal is Lbd2 .
Let q be given.
Assume Hq1 Hq2 .
We will prove q = x .
Assume Hq1a Hq1b Hq1c Hq1d .
We prove the intermediate
claim Lmq :
SNo (- q ) .
An
exact proof term for the current goal is
SNo_minus_SNo q Hq1c .
We prove the intermediate
claim Lxmq :
SNo (x + - q ) .
An
exact proof term for the current goal is
SNo_add_SNo x (- q ) Hx Lmq .
We prove the intermediate
claim Lqmx :
SNo (q + - x ) .
An
exact proof term for the current goal is
SNo_add_SNo q (- x ) Hq1c Lmx .
We prove the intermediate claim L5 : ∀w ∈ L , w < q .
Let w be given.
Assume Hw .
Let n be given.
Assume Hn .
Assume Hwn : w = f n .
rewrite the current goal using Hwn (from left to right).
We will prove f n < q .
Apply SNoLtLe_or (f n ) q (Lf n Hn ) Hq1c to the current goal.
Assume H9 : f n < q .
An exact proof term for the current goal is H9 .
Assume H9 : q ≤ f n .
Assume _ _ _ _ _ .
Assume _ .
We prove the intermediate
claim L5a :
SNo (f (ordsucc n ) ) .
We prove the intermediate
claim L5b :
q < f (ordsucc n ) .
We prove the intermediate
claim L5c :
0 < f (ordsucc n ) + - q .
We prove the intermediate
claim L5d :
SNo (f (ordsucc n ) + - q ) .
We prove the intermediate
claim L5e :
f (ordsucc n ) < x .
We prove the intermediate claim L5f : q < x .
An
exact proof term for the current goal is
SNoLt_tra q (f (ordsucc n ) ) x Hq1c L5a Hx L5b L5e .
We prove the intermediate claim L5g : 0 < x + - q .
An
exact proof term for the current goal is
SNoLt_minus_pos q x Hq1c Hx L5f .
We prove the intermediate
claim L5h :
abs_SNo (q + - x ) = x + - q .
An
exact proof term for the current goal is
pos_abs_SNo (x + - q ) L5g .
We prove the intermediate
claim L5i :
q = f (ordsucc n ) .
Apply Hfn2 q Hq1 to the current goal.
Let k be given.
rewrite the current goal using
pos_abs_SNo (f (ordsucc n ) + - q ) L5c (from left to right).
We will
prove f (ordsucc n ) + - q < x + - q .
An exact proof term for the current goal is L5e .
We will
prove x + - q < eps_ k .
rewrite the current goal using L5h (from right to left).
An exact proof term for the current goal is Hq2 k Hk .
rewrite the current goal using L5i (from left to right) at position 2.
An exact proof term for the current goal is L5b .
We prove the intermediate claim L6 : ∀z ∈ R , q < z .
Let z be given.
Assume Hz : z ∈ R .
Let m be given.
Assume Hm .
Assume Hzm : z = g m .
rewrite the current goal using Hzm (from left to right).
We will prove q < g m .
Apply SNoLtLe_or q (g m ) Hq1c (Lg m Hm ) to the current goal.
Assume H9 : q < g m .
An exact proof term for the current goal is H9 .
Assume H9 : g m ≤ q .
Assume _ _ _ _ _ .
Assume _ .
We prove the intermediate
claim L6a :
SNo (g (ordsucc m ) ) .
We prove the intermediate
claim L6b :
g (ordsucc m ) < q .
An exact proof term for the current goal is H9 .
We prove the intermediate
claim L6c :
0 < q + - g (ordsucc m ) .
We prove the intermediate
claim L6d :
SNo (q + - g (ordsucc m ) ) .
We prove the intermediate
claim L6e :
x < g (ordsucc m ) .
We prove the intermediate claim L6f : x < q .
An
exact proof term for the current goal is
SNoLt_tra x (g (ordsucc m ) ) q Hx L6a Hq1c L6e L6b .
We prove the intermediate claim L6g : 0 < q + - x .
An
exact proof term for the current goal is
SNoLt_minus_pos x q Hx Hq1c L6f .
We prove the intermediate
claim L6h :
abs_SNo (q + - x ) = q + - x .
An
exact proof term for the current goal is
pos_abs_SNo (q + - x ) L6g .
We prove the intermediate
claim L6i :
q = g (ordsucc m ) .
Apply Hgm2 q Hq1 to the current goal.
Let k be given.
rewrite the current goal using
pos_abs_SNo (q + - g (ordsucc m ) ) L6c (from left to right).
We will
prove q + - g (ordsucc m ) < q + - x .
We will
prove - g (ordsucc m ) < - x .
An exact proof term for the current goal is L6e .
We will
prove q + - x < eps_ k .
rewrite the current goal using L6h (from right to left).
An exact proof term for the current goal is Hq2 k Hk .
rewrite the current goal using L6i (from left to right) at position 1.
An exact proof term for the current goal is L6b .
Apply H7 q Hq1c L5 L6 to the current goal.
rewrite the current goal using Hxfg (from right to left).
rewrite the current goal using H8 (from left to right).
Apply H9 to the current goal.
An exact proof term for the current goal is Hq1a .
∎
Theorem. (SNo_approx_real_rep ) The following is provable:
∀x ∈ real , ∀p : prop , (∀f g ∈ SNoS_ ω ω , (∀n ∈ ω , f n < x ) → (∀n ∈ ω , x < f n + eps_ n ) → (∀n ∈ ω , ∀i ∈ n , f i < f n ) → (∀n ∈ ω , g n + - eps_ n < x ) → (∀n ∈ ω , x < g n ) → (∀n ∈ ω , ∀i ∈ n , g n < g i ) → SNoCutP {f n |n ∈ ω } {g n |n ∈ ω } → x = SNoCut {f n |n ∈ ω } {g n |n ∈ ω } → p ) → p
Proof: Let x be given.
Assume Hx .
Let p be given.
Assume Hp .
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 _ _ Hx4 Hx5 .
Let f be given.
Assume Hf .
Apply Hf to the current goal.
Assume Hf1 Hf2 .
Let g be given.
Assume Hg .
Apply Hg to the current goal.
Assume Hg1 Hg2 .
We prove the intermediate
claim Lf :
∀n ∈ ω , SNo (f n ) .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lg :
∀n ∈ ω , SNo (g n ) .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lf1 :
∀n ∈ ω , f n < x .
Let n be given.
Assume Hn .
Apply Hf2 n Hn to the current goal.
Assume H _ .
Apply H to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lf2 :
∀n ∈ ω , x < f n + eps_ n .
Let n be given.
Assume Hn .
Apply Hf2 n Hn to the current goal.
Assume H _ .
Apply H to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lf3 :
∀n ∈ ω , ∀i ∈ n , f i < f n .
Let n be given.
Assume Hn .
Apply Hf2 n Hn to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lg1 :
∀n ∈ ω , g n + - eps_ n < x .
Let n be given.
Assume Hn .
Apply Hg2 n Hn to the current goal.
Assume H _ .
Apply H to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lg2 :
∀n ∈ ω , x < g n .
Let n be given.
Assume Hn .
Apply Hg2 n Hn to the current goal.
Assume H _ .
Apply H to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lg3 :
∀n ∈ ω , ∀i ∈ n , g n < g i .
Let n be given.
Assume Hn .
Apply Hg2 n Hn to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lfg :
∀n m ∈ ω , f n < g m .
Let n be given.
Assume Hn .
Let m be given.
Assume Hm .
Apply SNoLt_tra (f n ) x (g m ) (Lf n Hn ) Hx1 (Lg m Hm ) to the current goal.
We will prove f n < x .
An exact proof term for the current goal is Lf1 n Hn .
We will prove x < g m .
An exact proof term for the current goal is Lg2 m Hm .
Set L to be the term
{f n |n ∈ ω } .
Set R to be the term
{g n |n ∈ ω } .
We prove the intermediate
claim Lxfg :
x = SNoCut L R .
rewrite the current goal using
SNo_eta x Hx1 (from left to right).
Let w be given.
Apply SNoL_E x Hx1 w Hw to the current goal.
Assume Hw3 : w < x .
We prove the intermediate
claim Lw1 :
w ∈ SNoS_ ω .
We prove the intermediate claim Lw2 : 0 < x + - w .
An
exact proof term for the current goal is
SNoLt_minus_pos w x Hw1 Hx1 Hw3 .
We prove the intermediate
claim Lw3 :
∃k ∈ ω , w + eps_ k ≤ x .
Apply dneg to the current goal.
We prove the intermediate claim Lw3a : w = x .
Apply Hx4 w Lw1 to the current goal.
Let k be given.
rewrite the current goal using
pos_abs_SNo (x + - w ) Lw2 (from left to right).
We will
prove x + - w < eps_ k .
An exact proof term for the current goal is H8 .
Apply H7 to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk .
We will
prove w + eps_ k ≤ x .
We will
prove w + eps_ k ≤ (x + - w ) + w .
We will
prove eps_ k + w ≤ (x + - w ) + w .
rewrite the current goal using Lw3a (from right to left) at position 1.
An exact proof term for the current goal is Hw3 .
Apply Lw3 to the current goal.
Let k be given.
Assume Hk .
Apply Hk to the current goal.
Apply SNoLt_tra w (f k ) (SNoCut L R ) Hw1 (Lf k Hk1 ) H2 to the current goal.
We will prove w < f k .
We will
prove w + eps_ k < f k + eps_ k .
We will
prove x < f k + eps_ k .
Apply Hf2 k Hk1 to the current goal.
Assume H _ .
Apply H to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
We will
prove f k < SNoCut L R .
An exact proof term for the current goal is H5 k Hk1 .
Let z be given.
Apply SNoR_E x Hx1 z Hz to the current goal.
Assume Hz3 : x < z .
We prove the intermediate
claim Lz1 :
z ∈ SNoS_ ω .
We prove the intermediate claim Lz2 : 0 < z + - x .
An
exact proof term for the current goal is
SNoLt_minus_pos x z Hx1 Hz1 Hz3 .
We prove the intermediate
claim Lz3 :
∃k ∈ ω , x + eps_ k ≤ z .
Apply dneg to the current goal.
We prove the intermediate claim Lz3a : z = x .
Apply Hx4 z Lz1 to the current goal.
Let k be given.
rewrite the current goal using
pos_abs_SNo (z + - x ) Lz2 (from left to right).
We will
prove z + - x < eps_ k .
An exact proof term for the current goal is H8 .
Apply H7 to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk .
We will
prove x + eps_ k ≤ z .
We will
prove x + eps_ k ≤ (z + - x ) + x .
We will
prove eps_ k + x ≤ (z + - x ) + x .
rewrite the current goal using Lz3a (from right to left) at position 2.
An exact proof term for the current goal is Hz3 .
Apply Lz3 to the current goal.
Let k be given.
Assume Hk .
Apply Hk to the current goal.
Apply SNoLt_tra (SNoCut L R ) (g k ) z H2 (Lg k Hk1 ) Hz1 to the current goal.
An exact proof term for the current goal is H6 k Hk1 .
We will prove g k < z .
We will
prove g k < x + eps_ k .
We will
prove g k + - eps_ k < x .
An exact proof term for the current goal is Lg1 k Hk1 .
We will
prove x + eps_ k ≤ z .
An exact proof term for the current goal is Hk2 .
Let w be given.
Assume Hw : w ∈ L .
rewrite the current goal using
SNo_eta x Hx1 (from right to left).
We will prove w < x .
Let n be given.
Assume Hn .
Assume Hwn : w = f n .
rewrite the current goal using Hwn (from left to right).
We will prove f n < x .
An exact proof term for the current goal is Lf1 n Hn .
Let z be given.
Assume Hz : z ∈ R .
rewrite the current goal using
SNo_eta x Hx1 (from right to left).
We will prove x < z .
Let m be given.
Assume Hm .
Assume Hzm : z = g m .
rewrite the current goal using Hzm (from left to right).
We will prove x < g m .
An exact proof term for the current goal is Lg2 m Hm .
An exact proof term for the current goal is Hp f Hf1 g Hg1 Lf1 Lf2 Lf3 Lg1 Lg2 Lg3 H1 Lxfg .
∎
Proof: Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
Let fL be given.
Assume HfL .
Let fR be given.
Assume HfR HfL1 HfL2 HfL3 HfR1 HfR2 HfR3 HfLR HxfLR .
Let gL be given.
Assume HgL .
Let gR be given.
Assume HgR HgL1 HgL2 HgL3 HgR1 HgR2 HgR3 HgLR HygLR .
Set L to be the term
{hL n |n ∈ ω } .
Set R to be the term
{hR n |n ∈ ω } .
We prove the intermediate
claim Lx :
SNo x .
An
exact proof term for the current goal is
real_SNo x Hx .
We prove the intermediate
claim Ly :
SNo y .
An
exact proof term for the current goal is
real_SNo y Hy .
We prove the intermediate
claim Lxy :
SNo (x + y ) .
An
exact proof term for the current goal is
SNo_add_SNo x y Lx Ly .
We prove the intermediate
claim Lx2 :
∀q ∈ SNoS_ ω , (∀k ∈ ω , abs_SNo (q + - x ) < eps_ k ) → q = x .
We prove the intermediate
claim Ly2 :
∀q ∈ SNoS_ ω , (∀k ∈ ω , abs_SNo (q + - y ) < eps_ k ) → q = y .
We prove the intermediate
claim LfLa :
∀n ∈ ω , fL (ordsucc n ) ∈ SNoS_ ω .
Let n be given.
Assume Hn .
We prove the intermediate
claim LfLb :
∀n ∈ ω , SNo (fL (ordsucc n ) ) .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim LgLa :
∀n ∈ ω , gL (ordsucc n ) ∈ SNoS_ ω .
Let n be given.
Assume Hn .
We prove the intermediate
claim LgLb :
∀n ∈ ω , SNo (gL (ordsucc n ) ) .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim LfRa :
∀n ∈ ω , fR (ordsucc n ) ∈ SNoS_ ω .
Let n be given.
Assume Hn .
We prove the intermediate
claim LfRb :
∀n ∈ ω , SNo (fR (ordsucc n ) ) .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim LgRa :
∀n ∈ ω , gR (ordsucc n ) ∈ SNoS_ ω .
Let n be given.
Assume Hn .
We prove the intermediate
claim LgRb :
∀n ∈ ω , SNo (gR (ordsucc n ) ) .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim LhL :
∀n ∈ ω , hL n = fL (ordsucc n ) + gL (ordsucc n ) .
Let n be given.
Assume Hn .
An
exact proof term for the current goal is
beta ω (λn ⇒ fL (ordsucc n ) + gL (ordsucc n ) ) n Hn .
We prove the intermediate
claim LhR :
∀n ∈ ω , hR n = fR (ordsucc n ) + gR (ordsucc n ) .
Let n be given.
Assume Hn .
An
exact proof term for the current goal is
beta ω (λn ⇒ fR (ordsucc n ) + gR (ordsucc n ) ) n Hn .
We prove the intermediate
claim LhLb :
∀n ∈ ω , SNo (hL n ) .
Let n be given.
Assume Hn .
rewrite the current goal using LhL n Hn (from left to right).
We prove the intermediate
claim LhRb :
∀n ∈ ω , SNo (hR n ) .
Let n be given.
Assume Hn .
rewrite the current goal using LhR n Hn (from left to right).
We prove the intermediate
claim L1 :
hL ∈ SNoS_ ω ω .
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn .
An exact proof term for the current goal is LfLa n Hn .
An exact proof term for the current goal is LgLa n Hn .
We prove the intermediate
claim L2 :
hR ∈ SNoS_ ω ω .
Apply lam_Pi to the current goal.
Let n be given.
Assume Hn .
An exact proof term for the current goal is LfRa n Hn .
An exact proof term for the current goal is LgRa n Hn .
We prove the intermediate
claim L3 :
∀n ∈ ω , hL n < x + y .
Let n be given.
Assume Hn .
rewrite the current goal using LhL n Hn (from left to right).
We prove the intermediate
claim L4 :
∀n ∈ ω , x + y < hL n + eps_ n .
Let n be given.
Assume Hn .
rewrite the current goal using LhL n Hn (from left to right).
We prove the intermediate
claim L5 :
∀n ∈ ω , ∀i ∈ n , hL i < hL n .
Let n be given.
Assume Hn .
Let i be given.
Assume Hi .
rewrite the current goal using LhL n Hn (from left to right).
We prove the intermediate
claim Li :
i ∈ ω .
rewrite the current goal using LhL i Li (from left to right).
We prove the intermediate
claim L6 :
∀n ∈ ω , hR n + - eps_ n < x + y .
Let n be given.
Assume Hn .
rewrite the current goal using LhR n Hn (from left to right).
We prove the intermediate
claim L7 :
∀n ∈ ω , x + y < hR n .
Let n be given.
Assume Hn .
rewrite the current goal using LhR n Hn (from left to right).
We prove the intermediate
claim L8 :
∀n ∈ ω , ∀i ∈ n , hR n < hR i .
Let n be given.
Assume Hn .
Let i be given.
Assume Hi .
rewrite the current goal using LhR n Hn (from left to right).
We prove the intermediate
claim Li :
i ∈ ω .
rewrite the current goal using LhR i Li (from left to right).
We prove the intermediate
claim LLR :
SNoCutP L R .
We will
prove (∀w ∈ L , SNo w ) ∧ (∀z ∈ R , SNo z ) ∧ (∀w ∈ L , ∀z ∈ R , w < z ) .
Apply and3I to the current goal.
Let w be given.
Assume Hw .
Let n be given.
Assume Hwn : w = hL n .
rewrite the current goal using Hwn (from left to right).
We will
prove SNo (hL n ) .
An exact proof term for the current goal is LhLb n Hn .
Let z be given.
Assume Hz .
Let m be given.
Assume Hzm : z = hR m .
rewrite the current goal using Hzm (from left to right).
We will
prove SNo (hR m ) .
An exact proof term for the current goal is LhRb m Hm .
Let w be given.
Assume Hw .
Let z be given.
Assume Hz .
Let n be given.
Assume Hwn : w = hL n .
rewrite the current goal using Hwn (from left to right).
Let m be given.
Assume Hzm : z = hR m .
rewrite the current goal using Hzm (from left to right).
We will prove hL n < hR m .
Apply SNoLt_tra (hL n ) (x + y ) (hR m ) (LhLb n Hn ) (SNo_add_SNo x y Lx Ly ) (LhRb m Hm ) to the current goal.
We will prove hL n < x + y .
An exact proof term for the current goal is L3 n Hn .
We will prove x + y < hR m .
An exact proof term for the current goal is L7 m Hm .
Assume HLR1 HLR2 HLR3 HLR4 HLR5 .
We prove the intermediate
claim L9 :
x + y = SNoCut L R .
rewrite the current goal using
add_SNo_eq x Lx y Ly (from left to right).
We will
prove ∀w ∈ {w + y |w ∈ SNoL x } ∪ {x + w |w ∈ SNoL y } , w < SNoCut L R .
Let w be given.
Assume Hw .
Let w' be given.
Assume Hww' .
rewrite the current goal using Hww' (from left to right).
We will
prove w' + y < SNoCut L R .
Apply SNoL_E x Lx w' Hw' to the current goal.
Assume Hw'1 Hw'2 Hw'3 .
We prove the intermediate
claim Lw'1 :
w' ∈ SNoS_ ω .
We prove the intermediate
claim Lw'2 :
∃n ∈ ω , w' + y ≤ hL n .
Apply dneg to the current goal.
We prove the intermediate claim Lw'2a : 0 < x + - w' .
We prove the intermediate claim Lw'2b : w' = x .
Apply Lx2 w' Lw'1 to the current goal.
Let k be given.
Assume Hk .
rewrite the current goal using
pos_abs_SNo (x + - w' ) Lw'2a (from left to right).
We will
prove x + - w' < eps_ k .
We will
prove x < eps_ k + w' .
Assume H2 .
An exact proof term for the current goal is H2 .
Apply HC to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk .
We will prove w' + y ≤ hL k .
We will prove w' + y < hL k .
We will
prove (w' + y ) + eps_ k < hL k + eps_ k .
We will
prove (w' + y ) + eps_ k ≤ x + y .
We will
prove (w' + eps_ k ) + y ≤ x + y .
We will
prove w' + eps_ k ≤ x .
We will
prove eps_ k + w' ≤ x .
An exact proof term for the current goal is H2 .
We will
prove x + y < hL k + eps_ k .
An exact proof term for the current goal is L4 k Hk .
We will prove x < x .
rewrite the current goal using Lw'2b (from right to left) at position 1.
An exact proof term for the current goal is Hw'3 .
Apply Lw'2 to the current goal.
Let n be given.
Assume Hn .
Apply Hn to the current goal.
Assume Hn1 Hn2 .
We will prove w' + y ≤ hL n .
An exact proof term for the current goal is Hn2 .
We will
prove hL n < SNoCut L R .
Apply HLR3 to the current goal.
We will prove hL n ∈ L .
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1 .
Let w' be given.
Assume Hww' .
rewrite the current goal using Hww' (from left to right).
We will
prove x + w' < SNoCut L R .
Apply SNoL_E y Ly w' Hw' to the current goal.
Assume Hw'1 Hw'2 Hw'3 .
We prove the intermediate
claim Lw'1 :
w' ∈ SNoS_ ω .
We prove the intermediate
claim Lw'2 :
∃n ∈ ω , x + w' ≤ hL n .
Apply dneg to the current goal.
We prove the intermediate claim Lw'2a : 0 < y + - w' .
We prove the intermediate claim Lw'2b : w' = y .
Apply Ly2 w' Lw'1 to the current goal.
Let k be given.
Assume Hk .
rewrite the current goal using
pos_abs_SNo (y + - w' ) Lw'2a (from left to right).
We will
prove y + - w' < eps_ k .
We will
prove y < eps_ k + w' .
Assume H2 .
An exact proof term for the current goal is H2 .
Apply HC to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk .
We will prove x + w' ≤ hL k .
We will prove x + w' < hL k .
We will
prove (x + w' ) + eps_ k < hL k + eps_ k .
We will
prove (x + w' ) + eps_ k ≤ x + y .
We will
prove x + (w' + eps_ k ) ≤ x + y .
We will
prove w' + eps_ k ≤ y .
We will
prove eps_ k + w' ≤ y .
An exact proof term for the current goal is H2 .
We will
prove x + y < hL k + eps_ k .
An exact proof term for the current goal is L4 k Hk .
We will prove y < y .
rewrite the current goal using Lw'2b (from right to left) at position 1.
An exact proof term for the current goal is Hw'3 .
Apply Lw'2 to the current goal.
Let n be given.
Assume Hn .
Apply Hn to the current goal.
Assume Hn1 Hn2 .
We will prove x + w' ≤ hL n .
An exact proof term for the current goal is Hn2 .
We will
prove hL n < SNoCut L R .
Apply HLR3 to the current goal.
We will prove hL n ∈ L .
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1 .
We will
prove ∀z ∈ {z + y |z ∈ SNoR x } ∪ {x + z |z ∈ SNoR y } , SNoCut L R < z .
Let z be given.
Assume Hz .
Let z' be given.
Assume Hzz' .
rewrite the current goal using Hzz' (from left to right).
We will
prove SNoCut L R < z' + y .
Apply SNoR_E x Lx z' Hz' to the current goal.
Assume Hz'1 Hz'2 Hz'3 .
We prove the intermediate
claim Lz'1 :
z' ∈ SNoS_ ω .
We prove the intermediate
claim Lz'2 :
∃n ∈ ω , hR n ≤ z' + y .
Apply dneg to the current goal.
We prove the intermediate claim Lz'2a : 0 < z' + - x .
We prove the intermediate claim Lz'2b : z' = x .
Apply Lx2 z' Lz'1 to the current goal.
Let k be given.
Assume Hk .
rewrite the current goal using
pos_abs_SNo (z' + - x ) Lz'2a (from left to right).
We will
prove z' + - x < eps_ k .
We will
prove z' < eps_ k + x .
Assume H2 .
An exact proof term for the current goal is H2 .
Apply HC to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk .
We will prove hR k ≤ z' + y .
We will
prove hR k + - eps_ k < (z' + y ) + - eps_ k .
We will
prove hR k + - eps_ k < x + y .
An exact proof term for the current goal is L6 k Hk .
We will
prove x + y ≤ (z' + y ) + - eps_ k .
We will
prove (x + y ) + eps_ k ≤ z' + y .
We will
prove (x + eps_ k ) + y ≤ z' + y .
We will
prove x + eps_ k ≤ z' .
An exact proof term for the current goal is H2 .
We will prove x < x .
rewrite the current goal using Lz'2b (from right to left) at position 2.
An exact proof term for the current goal is Hz'3 .
Apply Lz'2 to the current goal.
Let n be given.
Assume Hn .
Apply Hn to the current goal.
Assume Hn1 Hn2 .
We will
prove SNoCut L R < hR n .
Apply HLR4 to the current goal.
We will prove hR n ∈ R .
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1 .
We will prove hR n ≤ z' + y .
An exact proof term for the current goal is Hn2 .
Let z' be given.
Assume Hzz' .
rewrite the current goal using Hzz' (from left to right).
We will
prove SNoCut L R < x + z' .
Apply SNoR_E y Ly z' Hz' to the current goal.
Assume Hz'1 Hz'2 Hz'3 .
We prove the intermediate
claim Lz'1 :
z' ∈ SNoS_ ω .
We prove the intermediate
claim Lz'2 :
∃n ∈ ω , hR n ≤ x + z' .
Apply dneg to the current goal.
We prove the intermediate claim Lz'2a : 0 < z' + - y .
We prove the intermediate claim Lz'2b : z' = y .
Apply Ly2 z' Lz'1 to the current goal.
Let k be given.
Assume Hk .
rewrite the current goal using
pos_abs_SNo (z' + - y ) Lz'2a (from left to right).
We will
prove z' + - y < eps_ k .
We will
prove z' < eps_ k + y .
Assume H2 .
An exact proof term for the current goal is H2 .
Apply HC to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk .
We will prove hR k ≤ x + z' .
We will
prove hR k + - eps_ k < (x + z' ) + - eps_ k .
We will
prove hR k + - eps_ k < x + y .
An exact proof term for the current goal is L6 k Hk .
We will
prove x + y ≤ (x + z' ) + - eps_ k .
We will
prove (x + y ) + eps_ k ≤ x + z' .
We will
prove x + (y + eps_ k ) ≤ x + z' .
We will
prove y + eps_ k ≤ z' .
An exact proof term for the current goal is H2 .
We will prove y < y .
rewrite the current goal using Lz'2b (from right to left) at position 2.
An exact proof term for the current goal is Hz'3 .
Apply Lz'2 to the current goal.
Let n be given.
Assume Hn .
Apply Hn to the current goal.
Assume Hn1 Hn2 .
We will
prove SNoCut L R < hR n .
Apply HLR4 to the current goal.
We will prove hR n ∈ R .
Apply ReplI to the current goal.
An exact proof term for the current goal is Hn1 .
We will prove hR n ≤ x + z' .
An exact proof term for the current goal is Hn2 .
Let w be given.
Assume Hw : w ∈ L .
rewrite the current goal using
add_SNo_eq x Lx y Ly (from right to left).
We will prove w < x + y .
Let n be given.
Assume Hwn : w = hL n .
rewrite the current goal using Hwn (from left to right).
We will prove hL n < x + y .
An exact proof term for the current goal is L3 n Hn .
Let z be given.
Assume Hz : z ∈ R .
rewrite the current goal using
add_SNo_eq x Lx y Ly (from right to left).
We will prove x + y < z .
Let n be given.
Assume Hzn : z = hR n .
rewrite the current goal using Hzn (from left to right).
We will prove x + y < hR n .
An exact proof term for the current goal is L7 n Hn .
∎
Proof: Let x be given.
Assume Hx1 Hx2 Hx3 .
Assume Hx1a Hx1b Hx1c Hx1d .
Let N be given.
Assume HN .
Apply HN to the current goal.
Assume HN2 : x < N .
We prove the intermediate
claim LN :
SNo N .
An
exact proof term for the current goal is
omega_SNo N HN1 .
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1 .
We will
prove eps_ N * x < 1 .
We will prove x < N .
An exact proof term for the current goal is HN2 .
We will
prove eps_ N * N < 1 .
An exact proof term for the current goal is H1 .
We prove the intermediate
claim L2N :
SNo (2 ^ N ) .
We prove the intermediate
claim L1 :
2 ^ N ≤ 2 ^ N * eps_ N * N .
rewrite the current goal using
mul_SNo_oneR (2 ^ N ) L2N (from right to left) at position 1.
We will
prove 2 ^ N * 1 ≤ 2 ^ N * eps_ N * N .
An
exact proof term for the current goal is
SNo_1 .
We will
prove 1 ≤ eps_ N * N .
An exact proof term for the current goal is H1 .
We will prove 2 ^ N < 2 ^ N .
Apply SNoLeLt_tra (2 ^ N ) N (2 ^ N ) L2N LN L2N to the current goal.
We will prove 2 ^ N ≤ N .
rewrite the current goal using
mul_SNo_oneL N LN (from right to left) at position 2.
We will prove 2 ^ N ≤ 1 * N .
We will
prove 2 ^ N ≤ (2 ^ N * eps_ N ) * N .
An exact proof term for the current goal is L1 .
∎
Proof: Let x be given.
Assume Hx .
Let y be given.
Assume Hy Hx0 Hy0 .
Apply dneg to the current goal.
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 .
Apply real_E y Hy to the current goal.
Assume Hy1 Hy2 Hy3 Hy4 Hy5 Hy6 Hy7 .
We prove the intermediate
claim Lx7 :
∀k ∈ ω , ∀p : prop , (∀q ∈ SNoS_ ω , 0 < q → q < x → x < q + eps_ k → p ) → p .
We prove the intermediate
claim Ly7 :
∀k ∈ ω , ∀p : prop , (∀q ∈ SNoS_ ω , 0 < q → q < y → y < q + eps_ k → p ) → p .
We prove the intermediate
claim Lxy :
SNo (x * y ) .
An
exact proof term for the current goal is
SNo_mul_SNo x y Hx1 Hy1 .
We prove the intermediate
claim Lmxy :
SNo (- x * y ) .
An
exact proof term for the current goal is
SNo_minus_SNo (x * y ) Lxy .
We prove the intermediate
claim Lxy2 :
SNoLev (x * y ) ∉ ω .
Apply HC to the current goal.
We will
prove x * y ∈ SNoS_ ω .
An exact proof term for the current goal is Lxy .
Let q be given.
Assume Hq1 Hq2 .
Assume H1 .
An exact proof term for the current goal is H1 .
Apply Lxy2 to the current goal.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hq2 .
Apply Lxy2 to the current goal.
We prove the intermediate
claim LLx :
SNoL x ⊆ SNoS_ ω .
Let v be given.
Assume Hv .
Apply SNoL_E x Hx1 v Hv to the current goal.
Assume Hv3 .
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hv2 .
An exact proof term for the current goal is Hv1 .
We prove the intermediate
claim LRx :
SNoR x ⊆ SNoS_ ω .
Let v be given.
Assume Hv .
Apply SNoR_E x Hx1 v Hv to the current goal.
Assume Hv3 .
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hv2 .
An exact proof term for the current goal is Hv1 .
We prove the intermediate
claim LLy :
SNoL y ⊆ SNoS_ ω .
Let v be given.
Assume Hv .
Apply SNoL_E y Hy1 v Hv to the current goal.
Assume Hv3 .
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hv2 .
An exact proof term for the current goal is Hv1 .
We prove the intermediate
claim LRy :
SNoR y ⊆ SNoS_ ω .
Let v be given.
Assume Hv .
Apply SNoR_E y Hy1 v Hv to the current goal.
Assume Hv3 .
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hv2 .
An exact proof term for the current goal is Hv1 .
We prove the intermediate
claim LLx2 :
∀v ∈ SNoL x , ∀p : prop , (∀k, k ∈ ω → eps_ k ≤ x + - v → p ) → p .
Let v be given.
Assume Hv .
Let p be given.
Assume Hp .
Apply SNoL_E x Hx1 v Hv to the current goal.
Assume Hv3 : v < x .
Assume H1 .
We will prove x < x .
rewrite the current goal using Hx6 v (LLx v Hv ) H1 (from right to left) at position 1.
We will prove v < x .
An exact proof term for the current goal is Hv3 .
Apply dneg to the current goal.
Assume H2 : ¬ p .
Apply H1 to the current goal.
Let k be given.
We will
prove x + - v < eps_ k .
An exact proof term for the current goal is H3 .
Apply H2 to the current goal.
Apply Hp k Hk to the current goal.
An exact proof term for the current goal is H3 .
We prove the intermediate
claim LRx2 :
∀v ∈ SNoR x , ∀p : prop , (∀k, k ∈ ω → eps_ k ≤ v + - x → p ) → p .
Let v be given.
Assume Hv .
Let p be given.
Assume Hp .
Apply SNoR_E x Hx1 v Hv to the current goal.
Assume Hv3 : x < v .
Assume H1 .
We will prove x < x .
rewrite the current goal using Hx6 v (LRx v Hv ) H1 (from right to left) at position 2.
We will prove x < v .
An exact proof term for the current goal is Hv3 .
Apply dneg to the current goal.
Assume H2 : ¬ p .
Apply H1 to the current goal.
Let k be given.
We will
prove v + - x < eps_ k .
An exact proof term for the current goal is H3 .
Apply H2 to the current goal.
Apply Hp k Hk to the current goal.
An exact proof term for the current goal is H3 .
We prove the intermediate
claim LLy2 :
∀v ∈ SNoL y , ∀p : prop , (∀k, k ∈ ω → eps_ k ≤ y + - v → p ) → p .
Let v be given.
Assume Hv .
Let p be given.
Assume Hp .
Apply SNoL_E y Hy1 v Hv to the current goal.
Assume Hv3 : v < y .
Assume H1 .
We will prove y < y .
rewrite the current goal using Hy6 v (LLy v Hv ) H1 (from right to left) at position 1.
We will prove v < y .
An exact proof term for the current goal is Hv3 .
Apply dneg to the current goal.
Assume H2 : ¬ p .
Apply H1 to the current goal.
Let k be given.
We will
prove y + - v < eps_ k .
An exact proof term for the current goal is H3 .
Apply H2 to the current goal.
Apply Hp k Hk to the current goal.
An exact proof term for the current goal is H3 .
We prove the intermediate
claim LRy2 :
∀v ∈ SNoR y , ∀p : prop , (∀k, k ∈ ω → eps_ k ≤ v + - y → p ) → p .
Let v be given.
Assume Hv .
Let p be given.
Assume Hp .
Apply SNoR_E y Hy1 v Hv to the current goal.
Assume Hv3 : y < v .
Assume H1 .
We will prove y < y .
rewrite the current goal using Hy6 v (LRy v Hv ) H1 (from right to left) at position 2.
We will prove y < v .
An exact proof term for the current goal is Hv3 .
Apply dneg to the current goal.
Assume H2 : ¬ p .
Apply H1 to the current goal.
Let k be given.
We will
prove v + - y < eps_ k .
An exact proof term for the current goal is H3 .
Apply H2 to the current goal.
Apply Hp k Hk to the current goal.
An exact proof term for the current goal is H3 .
Let L and R be given.
We prove the intermediate
claim L1 :
∀q ∈ SNoS_ ω , (∀k ∈ ω , abs_SNo (q + - (x * y ) ) < eps_ k ) → q = x * y .
Let q be given.
Assume Hq1 Hq2 .
We will prove q = x * y .
Assume Hq1a Hq1b Hq1c Hq1d .
Assume H1 : q < x * y .
We prove the intermediate
claim Lq1 :
q ∈ SNoL (x * y ) .
Apply SNoL_I to the current goal.
An exact proof term for the current goal is Lxy .
An exact proof term for the current goal is Hq1c .
An exact proof term for the current goal is Lxy3 q Hq1c Hq1a .
We will prove q < x * y .
An exact proof term for the current goal is H1 .
Let v be given.
Let w be given.
Apply SNoL_E x Hx1 v Hv to the current goal.
Assume Hv1 _ _ .
Apply SNoL_E y Hy1 w Hw to the current goal.
Assume Hw1 _ _ .
Assume H2 : q + v * w ≤ v * y + x * w .
We prove the intermediate
claim Lvw :
SNo (v * w ) .
An
exact proof term for the current goal is
SNo_mul_SNo v w Hv1 Hw1 .
We prove the intermediate
claim Lxw :
SNo (x * w ) .
An
exact proof term for the current goal is
SNo_mul_SNo x w ?? Hw1 .
We prove the intermediate
claim Lmxw :
SNo (- x * w ) .
An
exact proof term for the current goal is
SNo_minus_SNo (x * w ) Lxw .
We prove the intermediate
claim Lvy :
SNo (v * y ) .
An
exact proof term for the current goal is
SNo_mul_SNo v y Hv1 ?? .
We prove the intermediate
claim Lmvy :
SNo (- v * y ) .
An
exact proof term for the current goal is
SNo_minus_SNo (v * y ) Lvy .
We prove the intermediate
claim Lxmv :
SNo (x + - v ) .
We prove the intermediate
claim Lymw :
SNo (y + - w ) .
Apply LLx2 v Hv to the current goal.
Let k be given.
Apply LLy2 w Hw to the current goal.
Let k' be given.
We prove the intermediate
claim Lek :
SNo (eps_ k ) .
An
exact proof term for the current goal is
SNo_eps_ k Hk1 .
We prove the intermediate
claim Lek' :
SNo (eps_ k' ) .
An
exact proof term for the current goal is
SNo_eps_ k' Hk'1 .
We prove the intermediate
claim Lkk' :
k + k' ∈ ω .
We prove the intermediate
claim Lekk' :
SNo (eps_ (k + k' ) ) .
An
exact proof term for the current goal is
SNo_eps_ (k + k' ) Lkk' .
We prove the intermediate
claim Lekek' :
SNo (eps_ k * eps_ k' ) .
We prove the intermediate
claim L1a :
abs_SNo (q + - (x * y ) ) < eps_ (k + k' ) .
An
exact proof term for the current goal is
Hq2 (k + k' ) (add_SNo_In_omega k Hk1 k' Hk'1 ) .
We prove the intermediate
claim L1b :
eps_ (k + k' ) ≤ abs_SNo (q + - (x * y ) ) .
rewrite the current goal using
abs_SNo_dist_swap q (x * y ) Hq1c Lxy (from left to right).
We will
prove eps_ (k + k' ) ≤ x * y + - q .
We will
prove eps_ (k + k' ) + q ≤ x * y .
We will
prove eps_ k * eps_ k' + q ≤ x * y .
We will
prove eps_ k * eps_ k' + q ≤ (x + - v ) * (y + - w ) + q .
We will
prove eps_ k * eps_ k' ≤ (x + - v ) * (y + - w ) .
We will
prove 0 ≤ eps_ k .
An
exact proof term for the current goal is
SNo_eps_pos k Hk1 .
We will
prove 0 ≤ eps_ k' .
An
exact proof term for the current goal is
SNo_eps_pos k' Hk'1 .
We will
prove eps_ k ≤ x + - v .
An exact proof term for the current goal is Hk2 .
We will
prove eps_ k' ≤ y + - w .
An exact proof term for the current goal is Hk'2 .
We will prove (x + - v ) * (y + - w ) + q ≤ x * y .
rewrite the current goal using
SNo_foil_mm x v y w Hx1 Hv1 Hy1 Hw1 (from left to right).
We will prove (x * y + - x * w + - v * y + v * w ) + q ≤ x * y .
rewrite the current goal using
add_SNo_assoc_4 (x * y ) (- x * w ) (- v * y ) (v * w ) ?? ?? ?? ?? (from left to right).
We will prove ((x * y + - x * w + - v * y ) + v * w ) + q ≤ x * y .
rewrite the current goal using
add_SNo_assoc (x * y + - x * w + - v * y ) (v * w ) q (SNo_add_SNo_3 (x * y ) (- x * w ) (- v * y ) ?? ?? ?? ) ?? Hq1c (from right to left).
We will prove (x * y + - x * w + - v * y ) + (v * w + q ) ≤ x * y .
rewrite the current goal using
add_SNo_com (v * w ) q ?? Hq1c (from left to right).
We will prove (x * y + - x * w + - v * y ) + (q + v * w ) ≤ x * y .
We will prove (x * y + - x * w + - v * y ) + (q + v * w ) ≤ (x * y + - x * w + - v * y ) + (v * y + x * w ) .
An
exact proof term for the current goal is
add_SNo_Le2 (x * y + - x * w + - v * y ) (q + v * w ) (v * y + x * w ) (SNo_add_SNo_3 (x * y ) (- x * w ) (- v * y ) ?? ?? ?? ) (SNo_add_SNo q (v * w ) Hq1c ?? ) (SNo_add_SNo (v * y ) (x * w ) ?? ?? ) H2 .
We will prove (x * y + - x * w + - v * y ) + (v * y + x * w ) ≤ x * y .
rewrite the current goal using
add_SNo_minus_SNo_prop5 (x * y ) (- x * w ) (v * y ) (x * w ) ?? ?? ?? ?? (from left to right).
We will prove x * y + - x * w + x * w ≤ x * y .
We will prove x * y + 0 ≤ x * y .
rewrite the current goal using
add_SNo_0R (x * y ) ?? (from left to right).
We will prove x * y ≤ x * y .
We will
prove eps_ (k + k' ) < eps_ (k + k' ) .
Let v be given.
Let w be given.
Apply SNoR_E x Hx1 v Hv to the current goal.
Assume Hv1 _ _ .
Apply SNoR_E y Hy1 w Hw to the current goal.
Assume Hw1 _ _ .
Assume H2 : q + v * w ≤ v * y + x * w .
We prove the intermediate
claim Lvw :
SNo (v * w ) .
An
exact proof term for the current goal is
SNo_mul_SNo v w Hv1 Hw1 .
We prove the intermediate
claim Lxw :
SNo (x * w ) .
An
exact proof term for the current goal is
SNo_mul_SNo x w ?? Hw1 .
We prove the intermediate
claim Lmxw :
SNo (- x * w ) .
An
exact proof term for the current goal is
SNo_minus_SNo (x * w ) Lxw .
We prove the intermediate
claim Lvy :
SNo (v * y ) .
An
exact proof term for the current goal is
SNo_mul_SNo v y Hv1 ?? .
We prove the intermediate
claim Lmvy :
SNo (- v * y ) .
An
exact proof term for the current goal is
SNo_minus_SNo (v * y ) Lvy .
We prove the intermediate
claim Lvmx :
SNo (v + - x ) .
We prove the intermediate
claim Lwmy :
SNo (w + - y ) .
Apply LRx2 v Hv to the current goal.
Let k be given.
Apply LRy2 w Hw to the current goal.
Let k' be given.
We prove the intermediate
claim Lek :
SNo (eps_ k ) .
An
exact proof term for the current goal is
SNo_eps_ k Hk1 .
We prove the intermediate
claim Lek' :
SNo (eps_ k' ) .
An
exact proof term for the current goal is
SNo_eps_ k' Hk'1 .
We prove the intermediate
claim Lkk' :
k + k' ∈ ω .
We prove the intermediate
claim Lekk' :
SNo (eps_ (k + k' ) ) .
An
exact proof term for the current goal is
SNo_eps_ (k + k' ) Lkk' .
We prove the intermediate
claim Lekek' :
SNo (eps_ k * eps_ k' ) .
We prove the intermediate
claim L1c :
abs_SNo (q + - (x * y ) ) < eps_ (k + k' ) .
An
exact proof term for the current goal is
Hq2 (k + k' ) (add_SNo_In_omega k Hk1 k' Hk'1 ) .
We prove the intermediate
claim L1d :
eps_ (k + k' ) ≤ abs_SNo (q + - (x * y ) ) .
rewrite the current goal using
abs_SNo_dist_swap q (x * y ) Hq1c Lxy (from left to right).
We will
prove eps_ (k + k' ) ≤ x * y + - q .
We will
prove eps_ (k + k' ) + q ≤ x * y .
We will
prove eps_ k * eps_ k' + q ≤ x * y .
We will
prove eps_ k * eps_ k' + q ≤ (v + - x ) * (w + - y ) + q .
We will
prove eps_ k * eps_ k' ≤ (v + - x ) * (w + - y ) .
We will
prove 0 ≤ eps_ k .
An
exact proof term for the current goal is
SNo_eps_pos k Hk1 .
We will
prove 0 ≤ eps_ k' .
An
exact proof term for the current goal is
SNo_eps_pos k' Hk'1 .
We will
prove eps_ k ≤ v + - x .
An exact proof term for the current goal is Hk2 .
We will
prove eps_ k' ≤ w + - y .
An exact proof term for the current goal is Hk'2 .
We will prove (v + - x ) * (w + - y ) + q ≤ x * y .
rewrite the current goal using
SNo_foil_mm v x w y Hv1 Hx1 Hw1 Hy1 (from left to right).
We will prove (v * w + - v * y + - x * w + x * y ) + q ≤ x * y .
rewrite the current goal using
add_SNo_assoc_4 (v * w ) (- v * y ) (- x * w ) (x * y ) ?? ?? ?? ?? (from left to right).
We will prove ((v * w + - v * y + - x * w ) + x * y ) + q ≤ x * y .
rewrite the current goal using
add_SNo_assoc (v * w + - v * y + - x * w ) (x * y ) q (SNo_add_SNo_3 (v * w ) (- v * y ) (- x * w ) ?? ?? ?? ) ?? Hq1c (from right to left).
We will prove (v * w + - v * y + - x * w ) + (x * y + q ) ≤ x * y .
rewrite the current goal using
add_SNo_com (x * y ) q ?? Hq1c (from left to right).
We will prove (v * w + - v * y + - x * w ) + (q + x * y ) ≤ x * y .
rewrite the current goal using
add_SNo_3a_2b (v * w ) (- v * y ) (- x * w ) q (x * y ) ?? ?? ?? ?? ?? (from left to right).
We will prove (x * y + - v * y + - x * w ) + (q + v * w ) ≤ x * y .
Apply SNoLe_tra ((x * y + - v * y + - x * w ) + (q + v * w ) ) ((x * y + - v * y + - x * w ) + (v * y + x * w ) ) (x * y ) (SNo_add_SNo (x * y + - v * y + - x * w ) (q + v * w ) (SNo_add_SNo_3 (x * y ) (- v * y ) (- x * w ) ?? ?? ?? ) (SNo_add_SNo q (v * w ) ?? ?? ) ) (SNo_add_SNo (x * y + - v * y + - x * w ) (v * y + x * w ) (SNo_add_SNo_3 (x * y ) (- v * y ) (- x * w ) ?? ?? ?? ) (SNo_add_SNo (v * y ) (x * w ) ?? ?? ) ) ?? to the current goal.
We will prove (x * y + - v * y + - x * w ) + (q + v * w ) ≤ (x * y + - v * y + - x * w ) + (v * y + x * w ) .
We will prove q + v * w ≤ v * y + x * w .
An exact proof term for the current goal is H2 .
We will prove (x * y + - v * y + - x * w ) + (v * y + x * w ) ≤ x * y .
rewrite the current goal using
add_SNo_com (v * y ) (x * w ) ?? ?? (from left to right).
We will prove (x * y + - v * y + - x * w ) + (x * w + v * y ) ≤ x * y .
rewrite the current goal using
add_SNo_minus_SNo_prop5 (x * y ) (- v * y ) (x * w ) (v * y ) ?? ?? ?? ?? (from left to right).
We will prove x * y + - v * y + v * y ≤ x * y .
We will prove x * y + 0 ≤ x * y .
rewrite the current goal using
add_SNo_0R (x * y ) ?? (from left to right).
We will
prove eps_ (k + k' ) < eps_ (k + k' ) .
Assume H1 : q = x * y .
An exact proof term for the current goal is H1 .
Assume H1 : x * y < q .
We prove the intermediate
claim Lq2 :
q ∈ SNoR (x * y ) .
Apply SNoR_I to the current goal.
An exact proof term for the current goal is Lxy .
An exact proof term for the current goal is Hq1c .
An exact proof term for the current goal is Lxy3 q Hq1c Hq1a .
We will prove x * y < q .
An exact proof term for the current goal is H1 .
Let v be given.
Let w be given.
Apply SNoL_E x Hx1 v Hv to the current goal.
Assume Hv1 _ _ .
Apply SNoR_E y Hy1 w Hw to the current goal.
Assume Hw1 _ _ .
Assume H2 : v * y + x * w ≤ q + v * w .
We prove the intermediate
claim Lvy :
SNo (v * y ) .
An
exact proof term for the current goal is
SNo_mul_SNo v y Hv1 Hy1 .
We prove the intermediate
claim Lxw :
SNo (x * w ) .
An
exact proof term for the current goal is
SNo_mul_SNo x w ?? Hw1 .
We prove the intermediate
claim Lmxw :
SNo (- x * w ) .
An
exact proof term for the current goal is
SNo_minus_SNo (x * w ) Lxw .
We prove the intermediate
claim Lvw :
SNo (v * w ) .
An
exact proof term for the current goal is
SNo_mul_SNo v w Hv1 ?? .
We prove the intermediate
claim Lmvw :
SNo (- v * w ) .
An
exact proof term for the current goal is
SNo_minus_SNo (v * w ) Lvw .
We prove the intermediate
claim Lxmv :
SNo (x + - v ) .
We prove the intermediate
claim Lwmy :
SNo (w + - y ) .
Apply LLx2 v Hv to the current goal.
Let k be given.
Apply LRy2 w Hw to the current goal.
Let k' be given.
We prove the intermediate
claim Lek :
SNo (eps_ k ) .
An
exact proof term for the current goal is
SNo_eps_ k Hk1 .
We prove the intermediate
claim Lek' :
SNo (eps_ k' ) .
An
exact proof term for the current goal is
SNo_eps_ k' Hk'1 .
We prove the intermediate
claim Lkk' :
k + k' ∈ ω .
We prove the intermediate
claim Lekk' :
SNo (eps_ (k + k' ) ) .
An
exact proof term for the current goal is
SNo_eps_ (k + k' ) Lkk' .
We prove the intermediate
claim Lekek' :
SNo (eps_ k * eps_ k' ) .
We prove the intermediate
claim L1e :
abs_SNo (q + - (x * y ) ) < eps_ (k + k' ) .
An
exact proof term for the current goal is
Hq2 (k + k' ) (add_SNo_In_omega k Hk1 k' Hk'1 ) .
We prove the intermediate
claim L1f :
eps_ (k + k' ) ≤ abs_SNo (q + - (x * y ) ) .
We will
prove eps_ (k + k' ) ≤ q + - x * y .
We will
prove eps_ (k + k' ) + x * y ≤ q .
We will
prove eps_ k * eps_ k' + x * y ≤ q .
We will
prove eps_ k * eps_ k' + x * y ≤ (x + - v ) * (w + - y ) + x * y .
We will
prove eps_ k * eps_ k' ≤ (x + - v ) * (w + - y ) .
We will
prove 0 ≤ eps_ k .
An
exact proof term for the current goal is
SNo_eps_pos k Hk1 .
We will
prove 0 ≤ eps_ k' .
An
exact proof term for the current goal is
SNo_eps_pos k' Hk'1 .
We will
prove eps_ k ≤ x + - v .
An exact proof term for the current goal is Hk2 .
We will
prove eps_ k' ≤ w + - y .
An exact proof term for the current goal is Hk'2 .
We will prove (x + - v ) * (w + - y ) + x * y ≤ q .
rewrite the current goal using
SNo_foil_mm x v w y Hx1 Hv1 Hw1 Hy1 (from left to right).
We will prove (x * w + - x * y + - v * w + v * y ) + x * y ≤ q .
rewrite the current goal using
add_SNo_rotate_4_1 (- x * y ) (- v * w ) (v * y ) (x * w ) ?? ?? ?? ?? (from right to left).
We will prove (- x * y + - v * w + v * y + x * w ) + x * y ≤ q .
rewrite the current goal using
add_SNo_com (- x * y + - v * w + v * y + x * w ) (x * y ) (SNo_add_SNo_4 (- x * y ) (- v * w ) (v * y ) (x * w ) ?? ?? ?? ?? ) ?? (from left to right).
rewrite the current goal using
add_SNo_minus_L2' (x * y ) (- v * w + v * y + x * w ) ?? (SNo_add_SNo_3 (- v * w ) (v * y ) (x * w ) ?? ?? ?? ) (from left to right).
We will prove - v * w + v * y + x * w ≤ q .
Apply SNoLe_tra (- v * w + v * y + x * w ) (- v * w + q + v * w ) q (SNo_add_SNo_3 (- v * w ) (v * y ) (x * w ) ?? ?? ?? ) (SNo_add_SNo_3 (- v * w ) q (v * w ) ?? ?? ?? ) Hq1c to the current goal.
We will prove - v * w + v * y + x * w ≤ - v * w + q + v * w .
An
exact proof term for the current goal is
add_SNo_Le2 (- v * w ) (v * y + x * w ) (q + v * w ) ?? (SNo_add_SNo (v * y ) (x * w ) ?? ?? ) (SNo_add_SNo q (v * w ) Hq1c ?? ) H2 .
We will prove - v * w + q + v * w ≤ q .
rewrite the current goal using
add_SNo_com q (v * w ) ?? ?? (from left to right).
rewrite the current goal using
add_SNo_minus_L2 (v * w ) q ?? ?? (from left to right).
We will prove q ≤ q .
We will
prove eps_ (k + k' ) < eps_ (k + k' ) .
Let v be given.
Let w be given.
Apply SNoR_E x Hx1 v Hv to the current goal.
Assume Hv1 _ _ .
Apply SNoL_E y Hy1 w Hw to the current goal.
Assume Hw1 _ _ .
Assume H2 : v * y + x * w ≤ q + v * w .
We prove the intermediate
claim Lvy :
SNo (v * y ) .
An
exact proof term for the current goal is
SNo_mul_SNo v y Hv1 Hy1 .
We prove the intermediate
claim Lxw :
SNo (x * w ) .
An
exact proof term for the current goal is
SNo_mul_SNo x w ?? Hw1 .
We prove the intermediate
claim Lvw :
SNo (v * w ) .
An
exact proof term for the current goal is
SNo_mul_SNo v w Hv1 ?? .
We prove the intermediate
claim Lmvw :
SNo (- v * w ) .
An
exact proof term for the current goal is
SNo_minus_SNo (v * w ) Lvw .
We prove the intermediate
claim Lvmx :
SNo (v + - x ) .
We prove the intermediate
claim Lymw :
SNo (y + - w ) .
Apply LRx2 v Hv to the current goal.
Let k be given.
Apply LLy2 w Hw to the current goal.
Let k' be given.
We prove the intermediate
claim Lek :
SNo (eps_ k ) .
An
exact proof term for the current goal is
SNo_eps_ k Hk1 .
We prove the intermediate
claim Lek' :
SNo (eps_ k' ) .
An
exact proof term for the current goal is
SNo_eps_ k' Hk'1 .
We prove the intermediate
claim Lkk' :
k + k' ∈ ω .
We prove the intermediate
claim Lekk' :
SNo (eps_ (k + k' ) ) .
An
exact proof term for the current goal is
SNo_eps_ (k + k' ) Lkk' .
We prove the intermediate
claim Lekek' :
SNo (eps_ k * eps_ k' ) .
We prove the intermediate
claim L1g :
abs_SNo (q + - (x * y ) ) < eps_ (k + k' ) .
An
exact proof term for the current goal is
Hq2 (k + k' ) (add_SNo_In_omega k Hk1 k' Hk'1 ) .
We prove the intermediate
claim L1h :
eps_ (k + k' ) ≤ abs_SNo (q + - (x * y ) ) .
We will
prove eps_ (k + k' ) ≤ q + - x * y .
We will
prove eps_ (k + k' ) + x * y ≤ q .
We will
prove eps_ k * eps_ k' + x * y ≤ q .
We will
prove eps_ k * eps_ k' + x * y ≤ (v + - x ) * (y + - w ) + x * y .
We will
prove eps_ k * eps_ k' ≤ (v + - x ) * (y + - w ) .
We will
prove 0 ≤ eps_ k .
An
exact proof term for the current goal is
SNo_eps_pos k Hk1 .
We will
prove 0 ≤ eps_ k' .
An
exact proof term for the current goal is
SNo_eps_pos k' Hk'1 .
We will
prove eps_ k ≤ v + - x .
An exact proof term for the current goal is Hk2 .
We will
prove eps_ k' ≤ y + - w .
An exact proof term for the current goal is Hk'2 .
We will prove (v + - x ) * (y + - w ) + x * y ≤ q .
rewrite the current goal using
SNo_foil_mm v x y w Hv1 Hx1 Hy1 Hw1 (from left to right).
We will prove (v * y + - v * w + - x * y + x * w ) + x * y ≤ q .
rewrite the current goal using
add_SNo_rotate_4_1 (v * y ) (- v * w ) (- x * y ) (x * w ) ?? ?? ?? ?? (from left to right).
rewrite the current goal using
add_SNo_rotate_4_1 (x * w ) (v * y ) (- v * w ) (- x * y ) ?? ?? ?? ?? (from left to right).
We will prove (- x * y + x * w + v * y + - v * w ) + x * y ≤ q .
rewrite the current goal using
add_SNo_com (- x * y + x * w + v * y + - v * w ) (x * y ) (SNo_add_SNo_4 (- x * y ) (x * w ) (v * y ) (- v * w ) ?? ?? ?? ?? ) ?? (from left to right).
We will prove x * y + - x * y + x * w + v * y + - v * w ≤ q .
rewrite the current goal using
add_SNo_minus_L2' (x * y ) (x * w + v * y + - v * w ) ?? (SNo_add_SNo_3 (x * w ) (v * y ) (- v * w ) ?? ?? ?? ) (from left to right).
We will prove x * w + v * y + - v * w ≤ q .
rewrite the current goal using
add_SNo_rotate_3_1 (x * w ) (v * y ) (- v * w ) ?? ?? ?? (from left to right).
We will prove - v * w + x * w + v * y ≤ q .
Apply SNoLe_tra (- v * w + x * w + v * y ) (- v * w + q + v * w ) q (SNo_add_SNo_3 (- v * w ) (x * w ) (v * y ) ?? ?? ?? ) (SNo_add_SNo_3 (- v * w ) q (v * w ) ?? ?? ?? ) ?? to the current goal.
We will prove - v * w + x * w + v * y ≤ - v * w + q + v * w .
We will prove x * w + v * y ≤ q + v * w .
rewrite the current goal using
add_SNo_com (x * w ) (v * y ) ?? ?? (from left to right).
An exact proof term for the current goal is H2 .
We will prove - v * w + q + v * w ≤ q .
rewrite the current goal using
add_SNo_com q (v * w ) ?? ?? (from left to right).
We will prove - v * w + v * w + q ≤ q .
rewrite the current goal using
add_SNo_minus_L2 (v * w ) q ?? ?? (from left to right).
We will prove q ≤ q .
We will
prove eps_ (k + k' ) < eps_ (k + k' ) .
We prove the intermediate
claim LNex :
∃N ∈ ω , eps_ N * x < 1 ∧ eps_ N * y < 1 .
Let N be given.
Assume HN .
Apply HN to the current goal.
Let N' be given.
Assume HN' .
Apply HN' to the current goal.
Assume H1 : N ∈ N' .
We use N' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN'1 .
Apply andI to the current goal.
We will
prove eps_ N' * x < 1 .
An
exact proof term for the current goal is
SNo_eps_decr N' HN'1 N H1 .
An exact proof term for the current goal is HN2 .
An exact proof term for the current goal is HN'2 .
Assume H1 : N = N' .
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1 .
Apply andI to the current goal.
An exact proof term for the current goal is HN2 .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is HN'2 .
Assume H1 : N' ∈ N .
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN1 .
Apply andI to the current goal.
An exact proof term for the current goal is HN2 .
We will
prove eps_ N * y < 1 .
An
exact proof term for the current goal is
SNo_eps_decr N HN1 N' H1 .
An exact proof term for the current goal is HN'2 .
Apply LNex to the current goal.
Let N be given.
Assume HN .
Apply HN to the current goal.
Assume HN .
Apply HN to the current goal.
We prove the intermediate
claim L2 :
∀k ∈ ω , ∃q ∈ SNoS_ ω , q < x * y ∧ x * y < q + eps_ k .
Let k be given.
Assume Hk .
We prove the intermediate
claim Lek :
SNo (eps_ k ) .
An
exact proof term for the current goal is
SNo_eps_ k Hk .
We prove the intermediate
claim Lk1 :
k + 1 ∈ ω .
We prove the intermediate
claim Lk2 :
k + 2 ∈ ω .
Set k' to be the term N + k + 2 .
We prove the intermediate
claim Lk' :
k' ∈ ω .
We prove the intermediate
claim Lek' :
SNo (eps_ k' ) .
An
exact proof term for the current goal is
SNo_eps_ k' Lk' .
Apply Lx7 k' Lk' to the current goal.
Let q be given.
Assume Hqpos : 0 < q .
Assume Hq2 : q < x .
Assume Hq1a Hq1b Hq1c Hq1d .
Apply Ly7 k' Lk' to the current goal.
Let q' be given.
Assume Hq'pos : 0 < q' .
Assume Hq'2 : q' < y .
Assume Hq'1a Hq'1b Hq'1c Hq'1d .
We prove the intermediate
claim Lqq' :
SNo (q * q' ) .
An
exact proof term for the current goal is
SNo_mul_SNo q q' Hq1c Hq'1c .
We use (q * q' ) to witness the existential quantifier.
Apply andI to the current goal.
We will
prove q * q' ∈ SNoS_ ω .
Apply andI to the current goal.
We will prove q * q' < x * y .
An
exact proof term for the current goal is
pos_mul_SNo_Lt2 q q' x y Hq1c Hq'1c Hx1 Hy1 Hqpos Hq'pos Hq2 Hq'2 .
We will
prove x * y < q * q' + eps_ k .
We will
prove x * y < (q + eps_ k' ) * (q' + eps_ k' ) .
We will
prove (q + eps_ k' ) * (q' + eps_ k' ) < q * q' + eps_ k .
rewrite the current goal using
SNo_foil q (eps_ k' ) q' (eps_ k' ) Hq1c Lek' Hq'1c Lek' (from left to right).
We will
prove q * eps_ (N + k + 2 ) + eps_ (N + k + 2 ) * q' + eps_ (N + k + 2 ) * eps_ (N + k + 2 ) < eps_ k .
rewrite the current goal using
add_SNo_1_1_2 (from left to right).
We prove the intermediate
claim LeN :
SNo (eps_ N ) .
An
exact proof term for the current goal is
SNo_eps_ N HN1 .
We prove the intermediate
claim Lek1 :
SNo (eps_ (k + 1 ) ) .
An
exact proof term for the current goal is
SNo_eps_ (k + 1 ) Lk1 .
We prove the intermediate
claim Lek2 :
SNo (eps_ (k + 2 ) ) .
An
exact proof term for the current goal is
SNo_eps_ (k + 2 ) Lk2 .
We prove the intermediate
claim LeNek2 :
SNo (eps_ N * eps_ (k + 2 ) ) .
We prove the intermediate
claim LeNek2sq :
SNo ((eps_ N * eps_ (k + 2 ) ) * (eps_ N * eps_ (k + 2 ) ) ) .
rewrite the current goal using
add_SNo_assoc (eps_ (k + 2 ) ) (eps_ (k + 2 ) ) (eps_ (k + 1 ) ) Lek2 Lek2 Lek1 (from right to left).
rewrite the current goal using
mul_SNo_assoc q (eps_ N ) (eps_ (k + 2 ) ) Hq1c LeN Lek2 (from left to right).
We will
prove q * eps_ N < 1 .
We will
prove 0 < eps_ N .
An
exact proof term for the current goal is
SNo_eps_pos N HN1 .
We will prove q < x .
An exact proof term for the current goal is Hq2 .
We will
prove x * eps_ N < 1 .
rewrite the current goal using
mul_SNo_com x (eps_ N ) Hx1 LeN (from left to right).
An exact proof term for the current goal is HN2 .
We will
prove 0 < eps_ (k + 2 ) .
An
exact proof term for the current goal is
SNo_eps_pos (k + 2 ) Lk2 .
rewrite the current goal using
mul_SNo_assoc q' (eps_ N ) (eps_ (k + 2 ) ) Hq'1c LeN Lek2 (from left to right).
We will
prove q' * eps_ N < 1 .
We will
prove 0 < eps_ N .
An
exact proof term for the current goal is
SNo_eps_pos N HN1 .
We will prove q' < y .
An exact proof term for the current goal is Hq'2 .
We will
prove y * eps_ N < 1 .
rewrite the current goal using
mul_SNo_com y (eps_ N ) Hy1 LeN (from left to right).
An exact proof term for the current goal is HN3 .
We will
prove 0 < eps_ (k + 2 ) .
An
exact proof term for the current goal is
SNo_eps_pos (k + 2 ) Lk2 .
We will
prove eps_ N * eps_ (k + 2 ) ≤ 1 .
rewrite the current goal using
mul_SNo_oneL 1 SNo_1 (from right to left) at position 2.
We will
prove eps_ N * eps_ (k + 2 ) ≤ 1 * 1 .
We will
prove 0 ≤ eps_ N .
An
exact proof term for the current goal is
SNo_eps_pos N HN1 .
We will
prove 0 ≤ eps_ (k + 2 ) .
An
exact proof term for the current goal is
SNo_eps_pos (k + 2 ) Lk2 .
We will
prove eps_ N ≤ 1 .
An exact proof term for the current goal is HN1 .
We will
prove eps_ (k + 2 ) ≤ 1 .
An exact proof term for the current goal is Lk2 .
We will
prove 0 ≤ eps_ N * eps_ (k + 2 ) .
An
exact proof term for the current goal is
SNo_eps_pos N HN1 .
An
exact proof term for the current goal is
SNo_eps_pos (k + 2 ) Lk2 .
We will
prove eps_ N ≤ 1 .
An exact proof term for the current goal is HN1 .
We will
prove 0 ≤ eps_ (k + 2 ) .
An
exact proof term for the current goal is
SNo_eps_pos (k + 2 ) Lk2 .
We will
prove eps_ (k + 2 ) < eps_ (k + 1 ) .
We will prove k + 1 ∈ k + 2 .
We will prove k + 1 < k + 2 .
We will prove 1 < 2 .
An
exact proof term for the current goal is
SNoLt_1_2 .
Let hL be given.
Assume HhL .
Apply HhL to the current goal.
Let hR be given.
Assume HhR .
Apply HhR to the current goal.
We prove the intermediate
claim LhL :
∀n ∈ ω , SNo (hL n ) .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim LhR :
∀n ∈ ω , SNo (hR n ) .
Let n be given.
Assume Hn .
Assume _ _ H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim L3 :
∀n ∈ ω , hL n < x * y .
Let n be given.
Assume Hn .
Apply HhL2 n Hn to the current goal.
Assume H _ .
Apply H to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim L4 :
∀n ∈ ω , x * y < hR n .
Let n be given.
Assume Hn .
Apply HhR2 n Hn to the current goal.
Assume H _ .
Apply H to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
We prove the intermediate
claim L5 :
∀n m ∈ ω , hL n < hR m .
Let n be given.
Assume Hn .
Let m be given.
Assume Hm .
Apply SNoLt_tra (hL n ) (x * y ) (hR m ) (LhL n Hn ) Lxy (LhR m Hm ) to the current goal.
We will prove hL n < x * y .
An exact proof term for the current goal is L3 n Hn .
We will prove x * y < hR m .
An exact proof term for the current goal is L4 m Hm .
Assume _ _ .
We prove the intermediate
claim L6 :
∀n ∈ ω , x * y < hL n + eps_ n .
Let n be given.
Assume Hn .
Apply HhL2 n Hn to the current goal.
Assume H _ .
Apply H to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
We prove the intermediate
claim L7 :
∀n ∈ ω , ∀i ∈ n , hL i < hL n .
Let n be given.
Assume Hn .
Apply HhL2 n Hn to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
We prove the intermediate
claim L8 :
∀n ∈ ω , hR n + - eps_ n < x * y .
Let n be given.
Assume Hn .
Apply HhR2 n Hn to the current goal.
Assume H _ .
Apply H to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim L9 :
∀n ∈ ω , ∀i ∈ n , hR n < hR i .
Let n be given.
Assume Hn .
Apply HhR2 n Hn to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
We prove the intermediate
claim L10 :
x * y = SNoCut {hL n |n ∈ ω } {hR n |n ∈ ω } .
rewrite the current goal using HxyLR (from left to right).
Apply SNoCut_ext L R {hL n |n ∈ ω } {hR n |n ∈ ω } HLR HhLR1 to the current goal.
Let w be given.
Assume Hw : w ∈ L .
We will
prove w < SNoCut {hL n |n ∈ ω } {hR n |n ∈ ω } .
Apply HLE w Hw to the current goal.
Let w0 be given.
Let w1 be given.
Assume Hwe : w = w0 * y + x * w1 + - w0 * w1 .
Apply LLx2 w0 Hw0 to the current goal.
Let k0 be given.
Apply LLy2 w1 Hw1 to the current goal.
Let k1 be given.
Apply SNoL_E x Hx1 w0 Hw0 to the current goal.
Assume Hw03 : w0 < x .
Apply SNoL_E y Hy1 w1 Hw1 to the current goal.
Assume Hw13 : w1 < y .
We prove the intermediate
claim Lek0 :
SNo (eps_ k0 ) .
An
exact proof term for the current goal is
SNo_eps_ k0 Hk0 .
We prove the intermediate
claim Lek1 :
SNo (eps_ k1 ) .
An
exact proof term for the current goal is
SNo_eps_ k1 Hk1 .
We prove the intermediate
claim Lk0k1 :
k0 + k1 ∈ ω .
We prove the intermediate
claim Lek0k1 :
SNo (eps_ (k0 + k1 ) ) .
An
exact proof term for the current goal is
SNo_eps_ (k0 + k1 ) Lk0k1 .
We prove the intermediate
claim LhLk0k1 :
SNo (hL (k0 + k1 ) ) .
An exact proof term for the current goal is LhL (k0 + k1 ) Lk0k1 .
We prove the intermediate
claim Lw0y :
SNo (w0 * y ) .
An
exact proof term for the current goal is
SNo_mul_SNo w0 y Hw01 Hy1 .
We prove the intermediate
claim Lxw1 :
SNo (x * w1 ) .
An
exact proof term for the current goal is
SNo_mul_SNo x w1 Hx1 Hw11 .
We prove the intermediate
claim Lw0w1 :
SNo (w0 * w1 ) .
An
exact proof term for the current goal is
SNo_mul_SNo w0 w1 Hw01 Hw11 .
We prove the intermediate
claim Lmw0w1 :
SNo (- w0 * w1 ) .
An
exact proof term for the current goal is
SNo_minus_SNo (w0 * w1 ) Lw0w1 .
We prove the intermediate
claim Lw0yxw1mw0w1 :
SNo (w0 * y + x * w1 + - w0 * w1 ) .
An
exact proof term for the current goal is
SNo_add_SNo_3 (w0 * y ) (x * w1 ) (- w0 * w1 ) Lw0y Lxw1 Lmw0w1 .
rewrite the current goal using Hwe (from left to right).
Apply SNoLeLt_tra (w0 * y + x * w1 + - w0 * w1 ) (hL (k0 + k1 ) ) (SNoCut {hL n |n ∈ ω } {hR n |n ∈ ω } ) Lw0yxw1mw0w1 LhLk0k1 HhLR2 to the current goal.
We will prove w0 * y + x * w1 + - w0 * w1 ≤ hL (k0 + k1 ) .
Apply SNoLtLe_or (hL (k0 + k1 ) ) (w0 * y + x * w1 + - w0 * w1 ) LhLk0k1 Lw0yxw1mw0w1 to the current goal.
Assume H1 : hL (k0 + k1 ) < w0 * y + x * w1 + - w0 * w1 .
We will prove x * y < x * y .
Apply SNoLt_tra (x * y ) (hL (k0 + k1 ) + eps_ (k0 + k1 ) ) (x * y ) Lxy (SNo_add_SNo (hL (k0 + k1 ) ) (eps_ (k0 + k1 ) ) LhLk0k1 Lek0k1 ) Lxy (L6 (k0 + k1 ) Lk0k1 ) to the current goal.
We will
prove hL (k0 + k1 ) + eps_ (k0 + k1 ) < x * y .
Apply SNoLtLe_tra (hL (k0 + k1 ) + eps_ (k0 + k1 ) ) ((w0 * y + x * w1 + - w0 * w1 ) + eps_ (k0 + k1 ) ) (x * y ) (SNo_add_SNo (hL (k0 + k1 ) ) (eps_ (k0 + k1 ) ) LhLk0k1 Lek0k1 ) (SNo_add_SNo (w0 * y + x * w1 + - w0 * w1 ) (eps_ (k0 + k1 ) ) Lw0yxw1mw0w1 Lek0k1 ) Lxy to the current goal.
We will
prove hL (k0 + k1 ) + eps_ (k0 + k1 ) < (w0 * y + x * w1 + - w0 * w1 ) + eps_ (k0 + k1 ) .
Apply add_SNo_Lt1 (hL (k0 + k1 ) ) (eps_ (k0 + k1 ) ) (w0 * y + x * w1 + - w0 * w1 ) LhLk0k1 Lek0k1 Lw0yxw1mw0w1 to the current goal.
An exact proof term for the current goal is H1 .
We will
prove (w0 * y + x * w1 + - w0 * w1 ) + eps_ (k0 + k1 ) ≤ x * y .
rewrite the current goal using
add_SNo_com (w0 * y + x * w1 + - w0 * w1 ) (eps_ (k0 + k1 ) ) Lw0yxw1mw0w1 Lek0k1 (from left to right).
Apply add_SNo_minus_Le2 (x * y ) (w0 * y + x * w1 + - w0 * w1 ) (eps_ (k0 + k1 ) ) Lxy Lw0yxw1mw0w1 Lek0k1 to the current goal.
We will
prove eps_ (k0 + k1 ) ≤ x * y + - (w0 * y + x * w1 + - w0 * w1 ) .
rewrite the current goal using
add_SNo_com_3_0_1 (w0 * y ) (x * w1 ) (- w0 * w1 ) Lw0y Lxw1 Lmw0w1 (from left to right).
We will
prove eps_ (k0 + k1 ) ≤ x * y + - (x * w1 + w0 * y + - w0 * w1 ) .
rewrite the current goal using
minus_add_SNo_distr_3 (x * w1 ) (w0 * y ) (- w0 * w1 ) Lxw1 Lw0y Lmw0w1 (from left to right).
We will
prove eps_ (k0 + k1 ) ≤ x * y + - x * w1 + - w0 * y + - - w0 * w1 .
We will
prove eps_ (k0 + k1 ) ≤ x * y + - x * w1 + (- w0 ) * y + - (- w0 ) * w1 .
We will
prove eps_ (k0 + k1 ) ≤ x * y + x * (- w1 ) + (- w0 ) * y + (- w0 ) * (- w1 ) .
We will
prove eps_ (k0 + k1 ) ≤ (x + - w0 ) * (y + - w1 ) .
We will
prove eps_ k0 * eps_ k1 ≤ (x + - w0 ) * (y + - w1 ) .
We will
prove 0 ≤ eps_ k0 .
An
exact proof term for the current goal is
SNo_eps_pos k0 Hk0 .
We will
prove 0 ≤ eps_ k1 .
An
exact proof term for the current goal is
SNo_eps_pos k1 Hk1 .
We will
prove eps_ k0 ≤ x + - w0 .
An exact proof term for the current goal is Hk0b .
We will
prove eps_ k1 ≤ y + - w1 .
An exact proof term for the current goal is Hk1b .
Assume H1 : w0 * y + x * w1 + - w0 * w1 ≤ hL (k0 + k1 ) .
An exact proof term for the current goal is H1 .
We will
prove hL (k0 + k1 ) < SNoCut {hL n |n ∈ ω } {hR n |n ∈ ω } .
An exact proof term for the current goal is HhLR5 (k0 + k1 ) Lk0k1 .
Let z0 be given.
Let z1 be given.
Assume Hwe : w = z0 * y + x * z1 + - z0 * z1 .
Apply LRx2 z0 Hz0 to the current goal.
Let k0 be given.
Apply LRy2 z1 Hz1 to the current goal.
Let k1 be given.
Apply SNoR_E x Hx1 z0 Hz0 to the current goal.
Assume Hz03 : x < z0 .
Apply SNoR_E y Hy1 z1 Hz1 to the current goal.
Assume Hz13 : y < z1 .
We prove the intermediate
claim Lek0 :
SNo (eps_ k0 ) .
An
exact proof term for the current goal is
SNo_eps_ k0 Hk0 .
We prove the intermediate
claim Lek1 :
SNo (eps_ k1 ) .
An
exact proof term for the current goal is
SNo_eps_ k1 Hk1 .
We prove the intermediate
claim Lk0k1 :
k0 + k1 ∈ ω .
We prove the intermediate
claim Lek0k1 :
SNo (eps_ (k0 + k1 ) ) .
An
exact proof term for the current goal is
SNo_eps_ (k0 + k1 ) Lk0k1 .
We prove the intermediate
claim LhLk0k1 :
SNo (hL (k0 + k1 ) ) .
An exact proof term for the current goal is LhL (k0 + k1 ) Lk0k1 .
We prove the intermediate
claim Lz0y :
SNo (z0 * y ) .
An
exact proof term for the current goal is
SNo_mul_SNo z0 y Hz01 Hy1 .
We prove the intermediate
claim Lxz1 :
SNo (x * z1 ) .
An
exact proof term for the current goal is
SNo_mul_SNo x z1 Hx1 Hz11 .
We prove the intermediate
claim Lz0z1 :
SNo (z0 * z1 ) .
An
exact proof term for the current goal is
SNo_mul_SNo z0 z1 Hz01 Hz11 .
We prove the intermediate
claim Lmz0z1 :
SNo (- z0 * z1 ) .
An
exact proof term for the current goal is
SNo_minus_SNo (z0 * z1 ) Lz0z1 .
We prove the intermediate
claim Lz0yxz1mz0z1 :
SNo (z0 * y + x * z1 + - z0 * z1 ) .
An
exact proof term for the current goal is
SNo_add_SNo_3 (z0 * y ) (x * z1 ) (- z0 * z1 ) Lz0y Lxz1 Lmz0z1 .
rewrite the current goal using Hwe (from left to right).
Apply SNoLeLt_tra (z0 * y + x * z1 + - z0 * z1 ) (hL (k0 + k1 ) ) (SNoCut {hL n |n ∈ ω } {hR n |n ∈ ω } ) Lz0yxz1mz0z1 LhLk0k1 HhLR2 to the current goal.
We will prove z0 * y + x * z1 + - z0 * z1 ≤ hL (k0 + k1 ) .
Apply SNoLtLe_or (hL (k0 + k1 ) ) (z0 * y + x * z1 + - z0 * z1 ) LhLk0k1 Lz0yxz1mz0z1 to the current goal.
Assume H1 : hL (k0 + k1 ) < z0 * y + x * z1 + - z0 * z1 .
We will prove x * y < x * y .
Apply SNoLt_tra (x * y ) (hL (k0 + k1 ) + eps_ (k0 + k1 ) ) (x * y ) Lxy (SNo_add_SNo (hL (k0 + k1 ) ) (eps_ (k0 + k1 ) ) LhLk0k1 Lek0k1 ) Lxy (L6 (k0 + k1 ) Lk0k1 ) to the current goal.
We will
prove hL (k0 + k1 ) + eps_ (k0 + k1 ) < x * y .
Apply SNoLtLe_tra (hL (k0 + k1 ) + eps_ (k0 + k1 ) ) ((z0 * y + x * z1 + - z0 * z1 ) + eps_ (k0 + k1 ) ) (x * y ) (SNo_add_SNo (hL (k0 + k1 ) ) (eps_ (k0 + k1 ) ) LhLk0k1 Lek0k1 ) (SNo_add_SNo (z0 * y + x * z1 + - z0 * z1 ) (eps_ (k0 + k1 ) ) Lz0yxz1mz0z1 Lek0k1 ) Lxy to the current goal.
We will
prove hL (k0 + k1 ) + eps_ (k0 + k1 ) < (z0 * y + x * z1 + - z0 * z1 ) + eps_ (k0 + k1 ) .
Apply add_SNo_Lt1 (hL (k0 + k1 ) ) (eps_ (k0 + k1 ) ) (z0 * y + x * z1 + - z0 * z1 ) LhLk0k1 Lek0k1 Lz0yxz1mz0z1 to the current goal.
An exact proof term for the current goal is H1 .
We will
prove (z0 * y + x * z1 + - z0 * z1 ) + eps_ (k0 + k1 ) ≤ x * y .
rewrite the current goal using
add_SNo_com (z0 * y + x * z1 + - z0 * z1 ) (eps_ (k0 + k1 ) ) Lz0yxz1mz0z1 Lek0k1 (from left to right).
Apply add_SNo_minus_Le2 (x * y ) (z0 * y + x * z1 + - z0 * z1 ) (eps_ (k0 + k1 ) ) Lxy Lz0yxz1mz0z1 Lek0k1 to the current goal.
We will
prove eps_ (k0 + k1 ) ≤ x * y + - (z0 * y + x * z1 + - z0 * z1 ) .
rewrite the current goal using
add_SNo_com (x * y ) (- (z0 * y + x * z1 + - z0 * z1 ) ) Lxy (SNo_minus_SNo (z0 * y + x * z1 + - z0 * z1 ) Lz0yxz1mz0z1 ) (from left to right).
rewrite the current goal using
add_SNo_rotate_3_1 (z0 * y ) (x * z1 ) (- z0 * z1 ) Lz0y Lxz1 Lmz0z1 (from left to right).
rewrite the current goal using
minus_add_SNo_distr_3 (- z0 * z1 ) (z0 * y ) (x * z1 ) Lmz0z1 Lz0y Lxz1 (from left to right).
rewrite the current goal using
minus_SNo_invol (z0 * z1 ) Lz0z1 (from left to right).
We will
prove eps_ (k0 + k1 ) ≤ (z0 * z1 + - z0 * y + - x * z1 ) + x * y .
We will
prove eps_ (k0 + k1 ) ≤ z0 * z1 + - z0 * y + - x * z1 + x * y .
We will
prove eps_ (k0 + k1 ) ≤ z0 * z1 + z0 * (- y ) + (- x ) * z1 + x * y .
We will
prove eps_ (k0 + k1 ) ≤ z0 * z1 + z0 * (- y ) + (- x ) * z1 + (- x ) * (- y ) .
We will
prove eps_ (k0 + k1 ) ≤ (z0 + - x ) * (z1 + - y ) .
We will
prove eps_ k0 * eps_ k1 ≤ (z0 + - x ) * (z1 + - y ) .
We will
prove 0 ≤ eps_ k0 .
An
exact proof term for the current goal is
SNo_eps_pos k0 Hk0 .
We will
prove 0 ≤ eps_ k1 .
An
exact proof term for the current goal is
SNo_eps_pos k1 Hk1 .
We will
prove eps_ k0 ≤ z0 + - x .
An exact proof term for the current goal is Hk0b .
We will
prove eps_ k1 ≤ z1 + - y .
An exact proof term for the current goal is Hk1b .
Assume H1 : z0 * y + x * z1 + - z0 * z1 ≤ hL (k0 + k1 ) .
An exact proof term for the current goal is H1 .
We will
prove hL (k0 + k1 ) < SNoCut {hL n |n ∈ ω } {hR n |n ∈ ω } .
An exact proof term for the current goal is HhLR5 (k0 + k1 ) Lk0k1 .
Let z be given.
Assume Hz : z ∈ R .
We will
prove SNoCut {hL n |n ∈ ω } {hR n |n ∈ ω } < z .
Apply HRE z Hz to the current goal.
Let w0 be given.
Let z1 be given.
Assume Hze : z = w0 * y + x * z1 + - w0 * z1 .
Apply LLx2 w0 Hw0 to the current goal.
Let k0 be given.
Apply LRy2 z1 Hz1 to the current goal.
Let k1 be given.
Apply SNoL_E x Hx1 w0 Hw0 to the current goal.
Assume Hw03 : w0 < x .
Apply SNoR_E y Hy1 z1 Hz1 to the current goal.
Assume Hz13 : y < z1 .
We prove the intermediate
claim Lek0 :
SNo (eps_ k0 ) .
An
exact proof term for the current goal is
SNo_eps_ k0 Hk0 .
We prove the intermediate
claim Lek1 :
SNo (eps_ k1 ) .
An
exact proof term for the current goal is
SNo_eps_ k1 Hk1 .
We prove the intermediate
claim Lk0k1 :
k0 + k1 ∈ ω .
We prove the intermediate
claim Lek0k1 :
SNo (eps_ (k0 + k1 ) ) .
An
exact proof term for the current goal is
SNo_eps_ (k0 + k1 ) Lk0k1 .
We prove the intermediate
claim Lmek0k1 :
SNo (- eps_ (k0 + k1 ) ) .
We prove the intermediate
claim LhRk0k1 :
SNo (hR (k0 + k1 ) ) .
An exact proof term for the current goal is LhR (k0 + k1 ) Lk0k1 .
We prove the intermediate
claim Lw0y :
SNo (w0 * y ) .
An
exact proof term for the current goal is
SNo_mul_SNo w0 y Hw01 Hy1 .
We prove the intermediate
claim Lxz1 :
SNo (x * z1 ) .
An
exact proof term for the current goal is
SNo_mul_SNo x z1 Hx1 Hz11 .
We prove the intermediate
claim Lw0z1 :
SNo (w0 * z1 ) .
An
exact proof term for the current goal is
SNo_mul_SNo w0 z1 Hw01 Hz11 .
We prove the intermediate
claim Lmw0z1 :
SNo (- w0 * z1 ) .
An
exact proof term for the current goal is
SNo_minus_SNo (w0 * z1 ) Lw0z1 .
We prove the intermediate
claim Lw0yxz1mw0z1 :
SNo (w0 * y + x * z1 + - w0 * z1 ) .
An
exact proof term for the current goal is
SNo_add_SNo_3 (w0 * y ) (x * z1 ) (- w0 * z1 ) Lw0y Lxz1 Lmw0z1 .
rewrite the current goal using Hze (from left to right).
Apply SNoLtLe_tra (SNoCut {hL n |n ∈ ω } {hR n |n ∈ ω } ) (hR (k0 + k1 ) ) (w0 * y + x * z1 + - w0 * z1 ) HhLR2 LhRk0k1 Lw0yxz1mw0z1 to the current goal.
We will
prove SNoCut {hL n |n ∈ ω } {hR n |n ∈ ω } < hR (k0 + k1 ) .
An exact proof term for the current goal is HhLR6 (k0 + k1 ) Lk0k1 .
We will prove hR (k0 + k1 ) ≤ w0 * y + x * z1 + - w0 * z1 .
Apply SNoLtLe_or (w0 * y + x * z1 + - w0 * z1 ) (hR (k0 + k1 ) ) Lw0yxz1mw0z1 LhRk0k1 to the current goal.
Assume H1 : w0 * y + x * z1 + - w0 * z1 < hR (k0 + k1 ) .
We will prove x * y < x * y .
Apply SNoLt_tra (x * y ) (hR (k0 + k1 ) + - eps_ (k0 + k1 ) ) (x * y ) Lxy (SNo_add_SNo (hR (k0 + k1 ) ) (- eps_ (k0 + k1 ) ) LhRk0k1 Lmek0k1 ) Lxy to the current goal.
We will
prove x * y < hR (k0 + k1 ) + - eps_ (k0 + k1 ) .
Apply SNoLeLt_tra (x * y ) ((w0 * y + x * z1 + - w0 * z1 ) + - eps_ (k0 + k1 ) ) (hR (k0 + k1 ) + - eps_ (k0 + k1 ) ) Lxy (SNo_add_SNo (w0 * y + x * z1 + - w0 * z1 ) (- eps_ (k0 + k1 ) ) Lw0yxz1mw0z1 Lmek0k1 ) (SNo_add_SNo (hR (k0 + k1 ) ) (- eps_ (k0 + k1 ) ) LhRk0k1 Lmek0k1 ) to the current goal.
We will
prove x * y ≤ (w0 * y + x * z1 + - w0 * z1 ) + - eps_ (k0 + k1 ) .
Apply add_SNo_minus_Le2b (w0 * y + x * z1 + - w0 * z1 ) (eps_ (k0 + k1 ) ) (x * y ) Lw0yxz1mw0z1 Lek0k1 Lxy to the current goal.
We will
prove x * y + eps_ (k0 + k1 ) ≤ w0 * y + x * z1 + - w0 * z1 .
rewrite the current goal using
add_SNo_com (x * y ) (eps_ (k0 + k1 ) ) Lxy Lek0k1 (from left to right).
Apply add_SNo_minus_Le2 (w0 * y + x * z1 + - w0 * z1 ) (x * y ) (eps_ (k0 + k1 ) ) Lw0yxz1mw0z1 Lxy Lek0k1 to the current goal.
We will
prove eps_ (k0 + k1 ) ≤ (w0 * y + x * z1 + - w0 * z1 ) + - x * y .
rewrite the current goal using
add_SNo_rotate_3_1 (w0 * y ) (x * z1 ) (- w0 * z1 ) Lw0y Lxz1 Lmw0z1 (from left to right).
We will
prove eps_ (k0 + k1 ) ≤ (- w0 * z1 + w0 * y + x * z1 ) + - x * y .
rewrite the current goal using
add_SNo_assoc_4 (- w0 * z1 ) (w0 * y ) (x * z1 ) (- x * y ) Lmw0z1 Lw0y Lxz1 Lmxy (from right to left).
We will
prove eps_ (k0 + k1 ) ≤ - w0 * z1 + w0 * y + x * z1 + - x * y .
rewrite the current goal using
add_SNo_rotate_4_1 (- w0 * z1 ) (w0 * y ) (x * z1 ) (- x * y ) Lmw0z1 Lw0y Lxz1 Lmxy (from left to right).
We will
prove eps_ (k0 + k1 ) ≤ - x * y + - w0 * z1 + w0 * y + x * z1 .
rewrite the current goal using
add_SNo_rotate_4_1 (- x * y ) (- w0 * z1 ) (w0 * y ) (x * z1 ) Lmxy Lmw0z1 Lw0y Lxz1 (from left to right).
We will
prove eps_ (k0 + k1 ) ≤ x * z1 + - x * y + - w0 * z1 + w0 * y .
We will
prove eps_ (k0 + k1 ) ≤ x * z1 + x * (- y ) + (- w0 ) * z1 + (- w0 ) * (- y ) .
We will
prove eps_ k0 * eps_ k1 ≤ (x + - w0 ) * (z1 + - y ) .
We will
prove 0 ≤ eps_ k0 .
An
exact proof term for the current goal is
SNo_eps_pos k0 Hk0 .
We will
prove 0 ≤ eps_ k1 .
An
exact proof term for the current goal is
SNo_eps_pos k1 Hk1 .
We will
prove eps_ k0 ≤ x + - w0 .
An exact proof term for the current goal is Hk0b .
We will
prove eps_ k1 ≤ z1 + - y .
An exact proof term for the current goal is Hk1b .
We will
prove (w0 * y + x * z1 + - w0 * z1 ) + - eps_ (k0 + k1 ) < hR (k0 + k1 ) + - eps_ (k0 + k1 ) .
Apply add_SNo_Lt1 (w0 * y + x * z1 + - w0 * z1 ) (- eps_ (k0 + k1 ) ) (hR (k0 + k1 ) ) Lw0yxz1mw0z1 Lmek0k1 LhRk0k1 to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is L8 (k0 + k1 ) Lk0k1 .
Assume H1 : hR (k0 + k1 ) ≤ w0 * y + x * z1 + - w0 * z1 .
An exact proof term for the current goal is H1 .
Let z0 be given.
Let w1 be given.
Assume Hze : z = z0 * y + x * w1 + - z0 * w1 .
Apply LRx2 z0 Hz0 to the current goal.
Let k0 be given.
Apply LLy2 w1 Hw1 to the current goal.
Let k1 be given.
Apply SNoR_E x Hx1 z0 Hz0 to the current goal.
Assume Hz03 : x < z0 .
Apply SNoL_E y Hy1 w1 Hw1 to the current goal.
Assume Hw13 : w1 < y .
We prove the intermediate
claim Lek0 :
SNo (eps_ k0 ) .
An
exact proof term for the current goal is
SNo_eps_ k0 Hk0 .
We prove the intermediate
claim Lek1 :
SNo (eps_ k1 ) .
An
exact proof term for the current goal is
SNo_eps_ k1 Hk1 .
We prove the intermediate
claim Lk0k1 :
k0 + k1 ∈ ω .
We prove the intermediate
claim Lek0k1 :
SNo (eps_ (k0 + k1 ) ) .
An
exact proof term for the current goal is
SNo_eps_ (k0 + k1 ) Lk0k1 .
We prove the intermediate
claim Lmek0k1 :
SNo (- eps_ (k0 + k1 ) ) .
We prove the intermediate
claim LhRk0k1 :
SNo (hR (k0 + k1 ) ) .
An exact proof term for the current goal is LhR (k0 + k1 ) Lk0k1 .
We prove the intermediate
claim Lz0y :
SNo (z0 * y ) .
An
exact proof term for the current goal is
SNo_mul_SNo z0 y Hz01 Hy1 .
We prove the intermediate
claim Lxw1 :
SNo (x * w1 ) .
An
exact proof term for the current goal is
SNo_mul_SNo x w1 Hx1 Hw11 .
We prove the intermediate
claim Lz0w1 :
SNo (z0 * w1 ) .
An
exact proof term for the current goal is
SNo_mul_SNo z0 w1 Hz01 Hw11 .
We prove the intermediate
claim Lmz0w1 :
SNo (- z0 * w1 ) .
An
exact proof term for the current goal is
SNo_minus_SNo (z0 * w1 ) Lz0w1 .
We prove the intermediate
claim Lz0yxw1mz0w1 :
SNo (z0 * y + x * w1 + - z0 * w1 ) .
An
exact proof term for the current goal is
SNo_add_SNo_3 (z0 * y ) (x * w1 ) (- z0 * w1 ) Lz0y Lxw1 Lmz0w1 .
rewrite the current goal using Hze (from left to right).
Apply SNoLtLe_tra (SNoCut {hL n |n ∈ ω } {hR n |n ∈ ω } ) (hR (k0 + k1 ) ) (z0 * y + x * w1 + - z0 * w1 ) HhLR2 LhRk0k1 Lz0yxw1mz0w1 to the current goal.
We will
prove SNoCut {hL n |n ∈ ω } {hR n |n ∈ ω } < hR (k0 + k1 ) .
An exact proof term for the current goal is HhLR6 (k0 + k1 ) Lk0k1 .
We will prove hR (k0 + k1 ) ≤ z0 * y + x * w1 + - z0 * w1 .
Apply SNoLtLe_or (z0 * y + x * w1 + - z0 * w1 ) (hR (k0 + k1 ) ) Lz0yxw1mz0w1 LhRk0k1 to the current goal.
Assume H1 : z0 * y + x * w1 + - z0 * w1 < hR (k0 + k1 ) .
We will prove x * y < x * y .
Apply SNoLt_tra (x * y ) (hR (k0 + k1 ) + - eps_ (k0 + k1 ) ) (x * y ) Lxy (SNo_add_SNo (hR (k0 + k1 ) ) (- eps_ (k0 + k1 ) ) LhRk0k1 Lmek0k1 ) Lxy to the current goal.
We will
prove x * y < hR (k0 + k1 ) + - eps_ (k0 + k1 ) .
Apply SNoLeLt_tra (x * y ) ((z0 * y + x * w1 + - z0 * w1 ) + - eps_ (k0 + k1 ) ) (hR (k0 + k1 ) + - eps_ (k0 + k1 ) ) Lxy (SNo_add_SNo (z0 * y + x * w1 + - z0 * w1 ) (- eps_ (k0 + k1 ) ) Lz0yxw1mz0w1 Lmek0k1 ) (SNo_add_SNo (hR (k0 + k1 ) ) (- eps_ (k0 + k1 ) ) LhRk0k1 Lmek0k1 ) to the current goal.
We will
prove x * y ≤ (z0 * y + x * w1 + - z0 * w1 ) + - eps_ (k0 + k1 ) .
Apply add_SNo_minus_Le2b (z0 * y + x * w1 + - z0 * w1 ) (eps_ (k0 + k1 ) ) (x * y ) Lz0yxw1mz0w1 Lek0k1 Lxy to the current goal.
We will
prove x * y + eps_ (k0 + k1 ) ≤ z0 * y + x * w1 + - z0 * w1 .
rewrite the current goal using
add_SNo_com (x * y ) (eps_ (k0 + k1 ) ) Lxy Lek0k1 (from left to right).
Apply add_SNo_minus_Le2 (z0 * y + x * w1 + - z0 * w1 ) (x * y ) (eps_ (k0 + k1 ) ) Lz0yxw1mz0w1 Lxy Lek0k1 to the current goal.
We will
prove eps_ (k0 + k1 ) ≤ (z0 * y + x * w1 + - z0 * w1 ) + - x * y .
rewrite the current goal using
add_SNo_assoc_4 (z0 * y ) (x * w1 ) (- z0 * w1 ) (- x * y ) Lz0y Lxw1 Lmz0w1 Lmxy (from right to left).
We will
prove eps_ (k0 + k1 ) ≤ z0 * y + x * w1 + - z0 * w1 + - x * y .
rewrite the current goal using
add_SNo_rotate_3_1 (- z0 * w1 ) (- x * y ) (x * w1 ) Lmz0w1 Lmxy Lxw1 (from right to left).
We will
prove eps_ (k0 + k1 ) ≤ z0 * y + - z0 * w1 + - x * y + x * w1 .
We will
prove eps_ (k0 + k1 ) ≤ z0 * y + z0 * (- w1 ) + (- x ) * y + (- x ) * (- w1 ) .
We will
prove eps_ k0 * eps_ k1 ≤ (z0 + - x ) * (y + - w1 ) .
We will
prove 0 ≤ eps_ k0 .
An
exact proof term for the current goal is
SNo_eps_pos k0 Hk0 .
We will
prove 0 ≤ eps_ k1 .
An
exact proof term for the current goal is
SNo_eps_pos k1 Hk1 .
We will
prove eps_ k0 ≤ z0 + - x .
An exact proof term for the current goal is Hk0b .
We will
prove eps_ k1 ≤ y + - w1 .
An exact proof term for the current goal is Hk1b .
We will
prove (z0 * y + x * w1 + - z0 * w1 ) + - eps_ (k0 + k1 ) < hR (k0 + k1 ) + - eps_ (k0 + k1 ) .
Apply add_SNo_Lt1 (z0 * y + x * w1 + - z0 * w1 ) (- eps_ (k0 + k1 ) ) (hR (k0 + k1 ) ) Lz0yxw1mz0w1 Lmek0k1 LhRk0k1 to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is L8 (k0 + k1 ) Lk0k1 .
Assume H1 : hR (k0 + k1 ) ≤ z0 * y + x * w1 + - z0 * w1 .
An exact proof term for the current goal is H1 .
Let w be given.
rewrite the current goal using HxyLR (from right to left).
We will prove w < x * y .
Let n be given.
Assume Hn Hwn .
rewrite the current goal using Hwn (from left to right).
We will prove hL n < x * y .
An exact proof term for the current goal is L3 n Hn .
Let z be given.
rewrite the current goal using HxyLR (from right to left).
We will prove x * y < z .
Let n be given.
Assume Hn Hzn .
rewrite the current goal using Hzn (from left to right).
We will prove x * y < hR n .
An exact proof term for the current goal is L4 n Hn .
Apply HC to the current goal.
An
exact proof term for the current goal is
SNo_approx_real (x * y ) Lxy hL HhL1 hR HhR1 L3 L6 L7 L4 L9 L10 .
∎
Proof: Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
We prove the intermediate
claim Lx :
SNo x .
An
exact proof term for the current goal is
real_SNo x Hx .
We prove the intermediate
claim Ly :
SNo y .
An
exact proof term for the current goal is
real_SNo y Hy .
We prove the intermediate
claim Lxy :
SNo (x * y ) .
An
exact proof term for the current goal is
SNo_mul_SNo x y Lx Ly .
Assume H1 : x < 0 .
We prove the intermediate claim Lmx : 0 < - x .
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 H1 .
Assume H2 : y < 0 .
We will
prove x * y ∈ real .
We will
prove (- x ) * (- y ) ∈ real .
We will prove 0 < - y .
We will prove y < - 0 .
rewrite the current goal using
minus_SNo_0 (from left to right).
An exact proof term for the current goal is H2 .
Assume H2 : y = 0 .
rewrite the current goal using H2 (from left to right).
rewrite the current goal using
mul_SNo_zeroR x Lx (from left to right).
An
exact proof term for the current goal is
real_0 .
Assume H2 : 0 < y .
We will
prove x * y ∈ real .
rewrite the current goal using
minus_SNo_invol (x * y ) Lxy (from right to left).
We will
prove - - (x * y ) ∈ real .
We will
prove - ((- x ) * y ) ∈ real .
We will
prove (- x ) * y ∈ real .
Assume H1 : x = 0 .
We will
prove x * y ∈ real .
rewrite the current goal using H1 (from left to right).
rewrite the current goal using
mul_SNo_zeroL y Ly (from left to right).
An
exact proof term for the current goal is
real_0 .
Assume H1 : 0 < x .
Assume H2 : y < 0 .
rewrite the current goal using
minus_SNo_invol (x * y ) Lxy (from right to left).
We will
prove - - (x * y ) ∈ real .
We will
prove - (x * (- y ) ) ∈ real .
We will
prove x * (- y ) ∈ real .
We will prove 0 < - y .
We will prove y < - 0 .
rewrite the current goal using
minus_SNo_0 (from left to right).
An exact proof term for the current goal is H2 .
Assume H2 : y = 0 .
rewrite the current goal using H2 (from left to right).
rewrite the current goal using
mul_SNo_zeroR x Lx (from left to right).
An
exact proof term for the current goal is
real_0 .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz Hxy Hyxz .
We prove the intermediate claim L1 : 0 ≤ y + - x .
We will prove x + - x ≤ y + - x .
We prove the intermediate
claim L2 :
abs_SNo (y + - x ) = y + - x .
rewrite the current goal using L2 (from left to right).
We will prove y + - x < z .
We will prove y < z + x .
rewrite the current goal using
add_SNo_com z x Hz Hx (from left to right).
An exact proof term for the current goal is Hyxz .
∎
Proof: Let x be given.
Assume Hx Hxpos Hxsmall .
Apply dneg to the current goal.
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 .
Set L to be the term
{q ∈ SNoS_ ω |x * q < 1 } .
Set R to be the term
{q ∈ SNoS_ ω |1 < x * q } .
We prove the intermediate
claim LLE :
∀q ∈ L , ∀p : prop , (SNo q → SNoLev q ∈ ω → x * q < 1 → p ) → p .
Let q be given.
Assume Hq : q ∈ L .
Let p be given.
Assume Hp .
Apply SepE (SNoS_ ω ) (λq ⇒ x * q < 1 ) q Hq to the current goal.
Assume Hq1 Hq2 .
Assume Hq1a _ Hq1c _ .
An exact proof term for the current goal is Hp Hq1c Hq1a Hq2 .
We prove the intermediate
claim LRE :
∀q ∈ R , ∀p : prop , (SNo q → SNoLev q ∈ ω → 1 < x * q → p ) → p .
Let q be given.
Assume Hq : q ∈ R .
Let p be given.
Assume Hp .
Apply SepE (SNoS_ ω ) (λq ⇒ 1 < x * q ) q Hq to the current goal.
Assume Hq1 Hq2 .
Assume Hq1a _ Hq1c _ .
An exact proof term for the current goal is Hp Hq1c Hq1a Hq2 .
We prove the intermediate
claim LLR :
SNoCutP L R .
We will
prove (∀w ∈ L , SNo w ) ∧ (∀z ∈ R , SNo z ) ∧ (∀w ∈ L , ∀z ∈ R , w < z ) .
Apply and3I to the current goal.
Let w be given.
Assume Hw .
Apply LLE w Hw to the current goal.
Assume H _ _ .
An exact proof term for the current goal is H .
Let z be given.
Assume Hz .
Apply LRE z Hz to the current goal.
Assume H _ _ .
An exact proof term for the current goal is H .
Let w be given.
Assume Hw .
Let z be given.
Assume Hz .
Apply LLE w Hw to the current goal.
Assume _ .
Assume Hw3 : x * w < 1 .
Apply LRE z Hz to the current goal.
Assume _ .
Assume Hz3 : 1 < x * z .
We will prove w < z .
Assume H1 : w < z .
An exact proof term for the current goal is H1 .
Assume H1 : z ≤ w .
We will prove 1 < 1 .
We will prove x * z < 1 .
We will prove x * z ≤ x * w .
An exact proof term for the current goal is H1 .
We will prove x * w < 1 .
An exact proof term for the current goal is Hw3 .
Set y to be the term
SNoCut L R .
Assume HLR3 : ∀w ∈ L , w < y .
Assume HLR4 : ∀z ∈ R , y < z .
Assume HLR5 .
An exact proof term for the current goal is H1 .
We prove the intermediate
claim L1 :
ω ∈ SNoLev y .
Apply H1 to the current goal.
Let q be given.
Assume Hq : q ∈ L .
Apply LLE q Hq to the current goal.
Assume H _ _ .
An exact proof term for the current goal is H .
Let q be given.
Assume Hq : q ∈ R .
Apply LRE q Hq to the current goal.
Assume H _ _ .
An exact proof term for the current goal is H .
Let q be given.
Assume Hq : q ∈ L .
Apply LLE q Hq to the current goal.
Assume _ H _ .
An exact proof term for the current goal is H .
Let q be given.
Assume Hq : q ∈ R .
Apply LRE q Hq to the current goal.
Assume _ H _ .
An exact proof term for the current goal is H .
An exact proof term for the current goal is HLR1 .
We prove the intermediate
claim Ly :
y ∈ real .
Apply real_I to the current goal.
An exact proof term for the current goal is LyL .
We prove the intermediate claim L4 : 0 = x .
Apply Hx6 to the current goal.
Let k be given.
rewrite the current goal using
abs_SNo_minus x ?? (from left to right).
rewrite the current goal using
pos_abs_SNo x Hxpos (from left to right).
We will
prove x < eps_ k .
An exact proof term for the current goal is H2 .
rewrite the current goal using H1 (from right to left) at position 1.
We prove the intermediate
claim L2k :
nat_p (2 ^ k ) .
We prove the intermediate
claim L2k' :
SNo (2 ^ k ) .
An
exact proof term for the current goal is
nat_p_SNo (2 ^ k ) L2k .
We prove the intermediate
claim L2k1 :
2 ^ k + 1 ∈ ω .
An
exact proof term for the current goal is
nat_p_omega (2 ^ k ) L2k .
We will prove y < 2 ^ k + 1 .
Apply HLR4 to the current goal.
We will prove 2 ^ k + 1 ∈ R .
We will
prove 2 ^ k + 1 ∈ {q ∈ SNoS_ ω |1 < x * q } .
Apply SepI to the current goal.
We will
prove 2 ^ k + 1 ∈ SNoS_ ω .
We will prove 1 < x * (2 ^ k + 1 ) .
We will prove 1 < x * 2 ^ k + x * 1 .
rewrite the current goal using
mul_SNo_oneR x ?? (from left to right).
We will prove 1 < x * 2 ^ k + x .
We will prove 1 < 1 + x .
rewrite the current goal using
add_SNo_0R 1 SNo_1 (from right to left) at position 1.
We will prove 1 + 0 < 1 + x .
We will prove 1 + x ≤ x * 2 ^ k + x .
We will prove 1 ≤ x * 2 ^ k .
We will
prove eps_ k * 2 ^ k ≤ x * 2 ^ k .
An
exact proof term for the current goal is
SNo_eps_ k Hk .
An exact proof term for the current goal is ?? .
An exact proof term for the current goal is L2k' .
We will
prove eps_ k ≤ x .
An exact proof term for the current goal is H2 .
We will
prove 2 ^ k + 1 < ω .
We will
prove 2 ^ k + 1 ∈ ω .
An exact proof term for the current goal is L2k1 .
We will prove 0 < 0 .
rewrite the current goal using L4 (from left to right) at position 2.
An exact proof term for the current goal is Hxpos .
We will prove 0 < 0 .
We will prove 0 < y .
Apply HLR3 to the current goal.
We will prove 0 ∈ L .
We will
prove 0 ∈ {q ∈ SNoS_ ω |x * q < 1 } .
Apply SepI to the current goal.
We will prove x * 0 < 1 .
rewrite the current goal using
mul_SNo_zeroR x ?? (from left to right).
An
exact proof term for the current goal is
SNoLt_0_1 .
rewrite the current goal using H1 (from left to right).
rewrite the current goal using
minus_SNo_0 (from left to right).
Let q be given.
Assume Hq1a Hq1b Hq1c Hq1d .
We prove the intermediate
claim Lq :
q ∈ real .
We prove the intermediate
claim Lxq :
x * q ∈ real .
An
exact proof term for the current goal is
real_mul_SNo x Hx q Lq .
Apply real_E (x * q ) Lxq to the current goal.
Assume Hxq1 Hxq2 Hxq3 Hxq4 Hxq5 Hxq6 Hxq7 .
We prove the intermediate
claim Lmxq :
SNo (- x * q ) .
An
exact proof term for the current goal is
SNo_minus_SNo (x * q ) ?? .
We prove the intermediate
claim Lxq1 :
x * q < 1 → ∃n ∈ ω , x * q + eps_ n ≤ 1 .
Assume H1 : x * q < 1 .
Apply dneg to the current goal.
We prove the intermediate claim Lxq1a : 1 = x * q .
Let n be given.
We will
prove 1 + - x * q < eps_ n .
Assume H2 .
An exact proof term for the current goal is H2 .
Apply HC to the current goal.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn .
We will
prove x * q + eps_ n ≤ 1 .
We will
prove eps_ n + x * q ≤ 1 .
We will
prove eps_ n ≤ 1 + - x * q .
An exact proof term for the current goal is H2 .
We will prove 1 < 1 .
rewrite the current goal using Lxq1a (from left to right) at position 1.
An exact proof term for the current goal is H1 .
We prove the intermediate
claim L1xq :
1 < x * q → ∃n ∈ ω , 1 ≤ x * q + - eps_ n .
Assume H1 : 1 < x * q .
Apply dneg to the current goal.
We prove the intermediate claim L1xqa : 1 = x * q .
Let n be given.
We will
prove x * q + - 1 < eps_ n .
Assume H2 .
An exact proof term for the current goal is H2 .
Apply HC to the current goal.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn .
We will
prove 1 ≤ x * q + - eps_ n .
We will
prove 1 + eps_ n ≤ x * q .
We will
prove eps_ n + 1 ≤ x * q .
An exact proof term for the current goal is H2 .
We will prove 1 < 1 .
rewrite the current goal using L1xqa (from left to right) at position 2.
An exact proof term for the current goal is H1 .
We will prove q = y .
Assume H1 : q < y .
Assume H2 : x * q < 1 .
Apply Lxq1 H2 to the current goal.
Let n be given.
Assume H .
Apply H to the current goal.
We prove the intermediate
claim Lqeny :
q + eps_ n < y .
Apply HLR3 to the current goal.
We will
prove q + eps_ n ∈ L .
Apply SepI to the current goal.
We will
prove x * (q + eps_ n ) < 1 .
We will
prove x * q + x * eps_ n < 1 .
We will
prove x * q + x * eps_ n < x * q + eps_ n .
An exact proof term for the current goal is H3 .
We will
prove y < q + eps_ n .
We will
prove y < eps_ n + q .
We will
prove y + - q < eps_ n .
An exact proof term for the current goal is Hq2 n Hn .
Assume H2 : x * q = 1 .
Apply HC to the current goal.
We will
prove ∃y ∈ real , x * y = 1 .
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lq .
An exact proof term for the current goal is H2 .
Assume H2 : 1 < x * q .
Apply SNoLt_tra q y q ?? HLR1 ?? H1 to the current goal.
We will prove y < q .
Apply HLR4 to the current goal.
We will prove q ∈ R .
Apply SepI to the current goal.
An exact proof term for the current goal is Hq1 .
An exact proof term for the current goal is H2 .
Assume H1 : q = y .
An exact proof term for the current goal is H1 .
Assume H1 : y < q .
Assume H2 : x * q < 1 .
Apply SNoLt_tra q y q ?? HLR1 ?? to the current goal.
We will prove q < y .
Apply HLR3 to the current goal.
We will prove q ∈ L .
Apply SepI to the current goal.
An exact proof term for the current goal is Hq1 .
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H1 .
Assume H2 : x * q = 1 .
Apply HC to the current goal.
We will
prove ∃y ∈ real , x * y = 1 .
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lq .
An exact proof term for the current goal is H2 .
Assume H2 : 1 < x * q .
Apply L1xq H2 to the current goal.
Let n be given.
Assume H .
Apply H to the current goal.
We prove the intermediate
claim Lyqen :
y < q + - eps_ n .
Apply HLR4 to the current goal.
We will
prove q + - eps_ n ∈ R .
Apply SepI to the current goal.
We will
prove 1 < x * (q + - eps_ n ) .
We will
prove 1 < x * q + x * (- eps_ n ) .
We will
prove x * q + - eps_ n < x * q + x * (- eps_ n ) .
We will
prove - eps_ n < x * (- eps_ n ) .
We will
prove q + - eps_ n < y .
We will
prove q < y + eps_ n .
We will
prove q < eps_ n + y .
We will
prove q + - y < eps_ n .
An exact proof term for the current goal is Hq2 n Hn .
Apply real_E y Ly to the current goal.
Assume Hy1 Hy2 Hy3 Hy4 Hy5 Hy6 Hy7 .
We prove the intermediate
claim Lxy :
x * y ∈ real .
An
exact proof term for the current goal is
real_mul_SNo x Hx y Ly .
We prove the intermediate
claim Lxy' :
SNo (x * y ) .
An
exact proof term for the current goal is
real_SNo (x * y ) Lxy .
Apply real_E (x * y ) Lxy to the current goal.
Assume Hxy2 .
Assume Hxy3 .
Assume Hxy4 .
Assume Hxy5 .
Apply HC to the current goal.
We use y to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ly .
We will prove x * y = 1 .
Use symmetry.
Apply Hxy6 to the current goal.
Let k be given.
Let q be given.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume Hq2 : q < y .
Assume Hq1a Hq1b Hq1c Hq1d .
We prove the intermediate
claim Lxq :
SNo (x * q ) .
An
exact proof term for the current goal is
SNo_mul_SNo x q ?? ?? .
We prove the intermediate
claim L1mxq :
SNo (1 + - (x * q ) ) .
We prove the intermediate
claim Lxqmxy :
SNo (x * q + - (x * y ) ) .
An
exact proof term for the current goal is
SNo_eps_ k Hk .
An
exact proof term for the current goal is
SNo_abs_SNo (1 + - (x * q ) ) ?? .
An
exact proof term for the current goal is
SNo_abs_SNo (x * q + - (x * y ) ) ?? .
An exact proof term for the current goal is LeSk .
An exact proof term for the current goal is LeSk .
We will prove x * q ≤ 1 .
Assume H1 : 1 < x * q .
We will prove q < q .
Apply SNoLt_tra q y q ?? ?? ?? Hq2 to the current goal.
We will prove y < q .
Apply HLR4 to the current goal.
We will prove q ∈ R .
Apply SepI to the current goal.
An exact proof term for the current goal is Hq1 .
We will prove 1 < x * q .
An exact proof term for the current goal is H1 .
Assume H1 : x * q ≤ 1 .
An exact proof term for the current goal is H1 .
We will prove y < y .
Apply HLR3 to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is Hq1 .
An exact proof term for the current goal is H1 .
Assume H1 .
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is L1 .
rewrite the current goal using
abs_SNo_dist_swap (x * q ) (x * y ) Lxq Lxy' (from left to right).
We will prove x * q ≤ x * y .
We will prove x * q < x * y .
We will prove q < y .
An exact proof term for the current goal is Hq2 .
An exact proof term for the current goal is Hq3 .
An exact proof term for the current goal is L1 .
∎
Proof: Let x be given.
Assume Hx Hxpos .
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 .
Let N be given.
Assume H .
Apply H to the current goal.
We prove the intermediate
claim L1 :
eps_ N ∈ real .
We prove the intermediate
claim L2 :
0 < eps_ N * x .
Let y be given.
Assume H .
Apply H to the current goal.
We prove the intermediate
claim LN :
SNo (eps_ N ) .
An
exact proof term for the current goal is
SNo_eps_ N HN .
We use
(eps_ N * y ) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hy .
We will
prove x * (eps_ N * y ) = 1 .
We will
prove (x * eps_ N ) * y = 1 .
rewrite the current goal using
mul_SNo_com x (eps_ N ) ?? ?? (from left to right).
An exact proof term for the current goal is H2 .
∎
Proof: Let x be given.
Assume Hx .
Assume Hxnz : x ≠ 0 .
We prove the intermediate
claim Lx :
SNo x .
An
exact proof term for the current goal is
real_SNo x Hx .
Assume H1 : x < 0 .
We prove the intermediate claim L1 : 0 < - x .
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 H1 .
Let y be given.
Assume H2 .
Apply H2 to the current goal.
Assume H2 : (- x ) * y = 1 .
We use (- y ) to witness the existential quantifier.
Apply andI to the current goal.
We will prove x * (- y ) = 1 .
We will prove - (x * y ) = 1 .
An exact proof term for the current goal is H2 .
Assume H1 : x = 0 .
An exact proof term for the current goal is Hxnz H1 .
∎
Proof: Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
Assume Hxpos Hynneg .
Apply real_E x Hx to the current goal.
Assume Hx1 Hx2 Hx3 Hx4 Hx5 .
Assume Hx7 .
We prove the intermediate
claim L1 :
∃n ∈ ω , eps_ n ≤ x .
Apply dneg to the current goal.
We prove the intermediate claim L1a : 0 = x .
Let k be given.
rewrite the current goal using
abs_SNo_minus x Hx1 (from left to right).
rewrite the current goal using
pos_abs_SNo x Hxpos (from left to right).
We will
prove x < eps_ k .
Assume H1 .
An exact proof term for the current goal is H1 .
Apply HC to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk .
An exact proof term for the current goal is H1 .
rewrite the current goal using L1a (from right to left) at position 1.
An exact proof term for the current goal is Hxpos .
Apply L1 to the current goal.
Let n be given.
Assume Hn .
Apply Hn to the current goal.
We prove the intermediate
claim L2n :
nat_p (2 ^ n ) .
An
exact proof term for the current goal is
nat_2 .
An
exact proof term for the current goal is
omega_nat_p n Hn1 .
We prove the intermediate
claim L2nb :
SNo (2 ^ n ) .
We prove the intermediate claim L2nc : 0 ≤ 2 ^ n .
An exact proof term for the current goal is L2n .
An
exact proof term for the current goal is
SNo_0 .
rewrite the current goal using
SNoLev_0 (from left to right).
An exact proof term for the current goal is L2n .
We prove the intermediate claim L2 : 1 ≤ 2 ^ n * x .
We will
prove 2 ^ n * eps_ n ≤ 2 ^ n * x .
We will
prove eps_ n ≤ x .
An exact proof term for the current goal is Hn2 .
Apply real_E y Hy to the current goal.
Assume Hy1 Hy2 .
Assume Hy4 .
Assume Hy6 Hy7 .
Let N be given.
Assume HN .
Apply HN to the current goal.
Assume HN2 : y < N .
We use (N * 2 ^ n ) to witness the existential quantifier.
Apply andI to the current goal.
We will
prove N * 2 ^ n ∈ ω .
We will
prove N * 2 ^ n ∈ ω .
An
exact proof term for the current goal is
omega_nat_p N HN1 .
An exact proof term for the current goal is L2n .
We will prove y ≤ (N * 2 ^ n ) * x .
We prove the intermediate
claim LN1 :
SNo N .
An
exact proof term for the current goal is
omega_SNo N HN1 .
We prove the intermediate
claim LN2n :
SNo (N * 2 ^ n ) .
An exact proof term for the current goal is LN1 .
An exact proof term for the current goal is L2nb .
Apply SNoLe_tra y N ((N * 2 ^ n ) * x ) Hy1 LN1 (SNo_mul_SNo (N * 2 ^ n ) x LN2n Hx1 ) to the current goal.
We will prove y ≤ N .
An exact proof term for the current goal is HN2 .
We will prove N ≤ (N * 2 ^ n ) * x .
rewrite the current goal using
mul_SNo_oneR N LN1 (from right to left) at position 1.
We will prove N * 1 ≤ (N * 2 ^ n ) * x .
rewrite the current goal using
mul_SNo_assoc N (2 ^ n ) x LN1 L2nb Hx1 (from right to left).
We will prove N * 1 ≤ N * (2 ^ n * x ) .
We prove the intermediate claim LN2 : 0 ≤ N .
An
exact proof term for the current goal is
omega_nat_p N HN1 .
An
exact proof term for the current goal is
SNo_0 .
rewrite the current goal using
SNoLev_0 (from left to right).
An
exact proof term for the current goal is
omega_nat_p N HN1 .
We will
prove SNo (2 ^ n * x ) .
An
exact proof term for the current goal is
SNo_mul_SNo (2 ^ n ) x L2nb Hx1 .
We will prove 1 ≤ 2 ^ n * x .
An exact proof term for the current goal is L2 .
∎
Proof: Let a be given.
Assume Ha .
Let b be given.
Assume Hb H1 .
Apply dneg to the current goal.
We prove the intermediate
claim La1 :
∀n ∈ ω , SNo (a n ) .
Let n be given.
Assume Hn .
Assume H _ _ _ _ _ _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lb1 :
∀n ∈ ω , SNo (b n ) .
Let n be given.
Assume Hn .
Assume H _ _ _ _ _ _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim La2 :
∀n, nat_p n → ∀m ∈ n , a m ≤ a n .
Let m be given.
Assume Hm : m ∈ 0 .
An
exact proof term for the current goal is
EmptyE m Hm .
Let n be given.
Assume Hn .
Assume IHn : ∀m ∈ n , a m ≤ a n .
Let m be given.
We prove the intermediate
claim Ln :
n ∈ ω .
An
exact proof term for the current goal is
nat_p_omega n Hn .
We prove the intermediate
claim LSn :
ordsucc n ∈ ω .
We prove the intermediate
claim Lm :
m ∈ ω .
We prove the intermediate
claim LanSn :
a n ≤ a (ordsucc n ) .
Apply H1 n Ln to the current goal.
Assume H _ .
Apply H to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
Apply ordsuccE n m Hm to the current goal.
Assume H2 : m ∈ n .
We will prove a m ≤ a n .
An exact proof term for the current goal is IHn m H2 .
An exact proof term for the current goal is LanSn .
Assume H2 : m = n .
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is LanSn .
We prove the intermediate
claim Lb2 :
∀n, nat_p n → ∀m ∈ n , b n ≤ b m .
Let m be given.
Assume Hm : m ∈ 0 .
An
exact proof term for the current goal is
EmptyE m Hm .
Let n be given.
Assume Hn .
Assume IHn : ∀m ∈ n , b n ≤ b m .
Let m be given.
We prove the intermediate
claim Ln :
n ∈ ω .
An
exact proof term for the current goal is
nat_p_omega n Hn .
We prove the intermediate
claim LSn :
ordsucc n ∈ ω .
We prove the intermediate
claim Lm :
m ∈ ω .
We prove the intermediate
claim LbSnn :
b (ordsucc n ) ≤ b n .
Apply H1 n Ln to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
Apply ordsuccE n m Hm to the current goal.
Assume H2 : m ∈ n .
An exact proof term for the current goal is LbSnn .
We will prove b n ≤ b m .
An exact proof term for the current goal is IHn m H2 .
Assume H2 : m = n .
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is LbSnn .
We prove the intermediate
claim Lab :
∀n m ∈ ω , a n ≤ b m .
Let n be given.
Assume Hn .
Let m be given.
Assume Hm .
We prove the intermediate
claim Ln :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
We prove the intermediate
claim Lm :
nat_p m .
An
exact proof term for the current goal is
omega_nat_p m Hm .
We prove the intermediate claim Labn : a n ≤ b n .
Apply H1 n Hn to the current goal.
Assume H _ .
Apply H to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
Assume H2 : n ∈ m .
We will prove a n ≤ b m .
Apply SNoLe_tra (a n ) (a m ) (b m ) (La1 n Hn ) (La1 m Hm ) (Lb1 m Hm ) to the current goal.
We will prove a n ≤ a m .
An exact proof term for the current goal is La2 m Lm n H2 .
We will prove a m ≤ b m .
Apply H1 m Hm to the current goal.
Assume H _ .
Apply H to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
Assume H2 : n = m .
rewrite the current goal using H2 (from right to left).
We will prove a n ≤ b n .
An exact proof term for the current goal is Labn .
Assume H2 : m ∈ n .
We will prove a n ≤ b m .
Apply SNoLe_tra (a n ) (b n ) (b m ) (La1 n Hn ) (Lb1 n Hn ) (Lb1 m Hm ) to the current goal.
We will prove a n ≤ b n .
An exact proof term for the current goal is Labn .
We will prove b n ≤ b m .
An exact proof term for the current goal is Lb2 n Ln m H2 .
Set L to be the term
{q ∈ SNoS_ ω |∃n ∈ ω , q < a n } .
Set R to be the term
{q ∈ SNoS_ ω |∃n ∈ ω , b n < q } .
Set x to be the term
SNoCut L R .
We prove the intermediate
claim LL :
L ⊆ SNoS_ ω .
An
exact proof term for the current goal is
Sep_Subq (SNoS_ ω ) (λq ⇒ ∃n ∈ ω , q < a n ) .
We prove the intermediate
claim LR :
R ⊆ SNoS_ ω .
An
exact proof term for the current goal is
Sep_Subq (SNoS_ ω ) (λq ⇒ ∃n ∈ ω , b n < q ) .
We prove the intermediate
claim LLR :
SNoCutP L R .
We will
prove (∀w ∈ L , SNo w ) ∧ (∀y ∈ R , SNo y ) ∧ (∀w ∈ L , ∀y ∈ R , w < y ) .
Apply and3I to the current goal.
Let w be given.
Assume Hw : w ∈ L .
Apply SepE (SNoS_ ω ) (λq ⇒ ∃m ∈ ω , q < a m ) w Hw to the current goal.
Assume H3 .
Apply H3 to the current goal.
Let n be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : w < a n .
Assume Hw1 Hw2 Hw3 Hw4 .
An exact proof term for the current goal is Hw3 .
Let z be given.
Assume Hz : z ∈ R .
Apply SepE (SNoS_ ω ) (λq ⇒ ∃m ∈ ω , b m < q ) z Hz to the current goal.
Assume H3 .
Apply H3 to the current goal.
Let m be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : b m < z .
Assume Hz1 Hz2 Hz3 Hz4 .
An exact proof term for the current goal is Hz3 .
Let w be given.
Assume Hw : w ∈ L .
Let z be given.
Assume Hz : z ∈ R .
Apply SepE (SNoS_ ω ) (λq ⇒ ∃m ∈ ω , q < a m ) w Hw to the current goal.
Assume H3 .
Apply H3 to the current goal.
Let n be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : w < a n .
Assume Hw1 Hw2 Hw3 Hw4 .
Apply SepE (SNoS_ ω ) (λq ⇒ ∃m ∈ ω , b m < q ) z Hz to the current goal.
Assume H5 .
Apply H5 to the current goal.
Let m be given.
Assume H5 .
Apply H5 to the current goal.
Assume H5 : b m < z .
Assume Hz1 Hz2 Hz3 Hz4 .
We will prove w < z .
Apply SNoLt_tra w (a n ) z Hw3 (La1 n Hn ) Hz3 H3 to the current goal.
We will prove a n < z .
Apply SNoLeLt_tra (a n ) (b m ) z (La1 n Hn ) (Lb1 m Hm ) Hz3 to the current goal.
We will prove a n ≤ b m .
An exact proof term for the current goal is Lab n Hn m Hm .
We will prove b m < z .
An exact proof term for the current goal is H5 .
We prove the intermediate
claim Lax :
∀n ∈ ω , a n ≤ x .
Let n be given.
Assume Hn .
Let f be given.
Assume Hf .
Let g be given.
Assume Hg Hf1 Hf2 Hf3 Hg1 Hg2 Hg3 Hfg Hanfg .
rewrite the current goal using Hanfg (from left to right).
Apply SNoCut_Le {f m |m ∈ ω } {g m |m ∈ ω } L R to the current goal.
We will
prove SNoCutP {f m |m ∈ ω } {g m |m ∈ ω } .
An exact proof term for the current goal is Hfg .
An exact proof term for the current goal is LLR .
Let w be given.
We will prove w < x .
Let m be given.
Assume Hwm : w = f m .
rewrite the current goal using Hwm (from left to right).
We will prove f m < x .
Apply HLR3 to the current goal.
We will prove f m ∈ L .
Apply SepI to the current goal.
An
exact proof term for the current goal is
ap_Pi ω (λ_ ⇒ SNoS_ ω ) f m Hf Hm .
We will
prove ∃n ∈ ω , f m < a n .
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn .
An exact proof term for the current goal is Hf1 m Hm .
Let z be given.
Assume Hz : z ∈ R .
rewrite the current goal using Hanfg (from right to left).
We will prove a n < z .
Apply SepE (SNoS_ ω ) (λq ⇒ ∃m ∈ ω , b m < q ) z Hz to the current goal.
Assume H3 .
Apply H3 to the current goal.
Let m be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : b m < z .
Assume Hz1 Hz2 Hz3 Hz4 .
Apply SNoLeLt_tra (a n ) (b m ) z (La1 n Hn ) (Lb1 m Hm ) Hz3 to the current goal.
We will prove a n ≤ b m .
An exact proof term for the current goal is Lab n Hn m Hm .
An exact proof term for the current goal is H3 .
We prove the intermediate
claim Lxb :
∀n ∈ ω , x ≤ b n .
Let n be given.
Assume Hn .
We will prove x ≤ b n .
Let f be given.
Assume Hf .
Let g be given.
Assume Hg Hf1 Hf2 Hf3 Hg1 Hg2 Hg3 Hfg Hbnfg .
rewrite the current goal using Hbnfg (from left to right).
Apply SNoCut_Le L R {f m |m ∈ ω } {g m |m ∈ ω } to the current goal.
An exact proof term for the current goal is LLR .
We will
prove SNoCutP {f m |m ∈ ω } {g m |m ∈ ω } .
An exact proof term for the current goal is Hfg .
Let w be given.
Assume Hw : w ∈ L .
rewrite the current goal using Hbnfg (from right to left).
We will prove w < b n .
Apply SepE (SNoS_ ω ) (λq ⇒ ∃m ∈ ω , q < a m ) w Hw to the current goal.
Assume H3 .
Apply H3 to the current goal.
Let m be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : w < a m .
Assume Hw1 Hw2 Hw3 Hw4 .
Apply SNoLtLe_tra w (a m ) (b n ) Hw3 (La1 m Hm ) (Lb1 n Hn ) to the current goal.
An exact proof term for the current goal is H3 .
We will prove a m ≤ b n .
An exact proof term for the current goal is Lab m Hm n Hn .
Let z be given.
We will prove x < z .
Let m be given.
Assume Hzm : z = g m .
rewrite the current goal using Hzm (from left to right).
We will prove x < g m .
Apply HLR4 to the current goal.
We will prove g m ∈ R .
Apply SepI to the current goal.
An
exact proof term for the current goal is
ap_Pi ω (λ_ ⇒ SNoS_ ω ) g m Hg Hm .
We will
prove ∃n ∈ ω , b n < g m .
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn .
An exact proof term for the current goal is Hg2 m Hm .
We prove the intermediate
claim Laxb :
∀n ∈ ω , a n ≤ x ∧ x ≤ b n .
Let n be given.
Assume Hn .
Apply andI to the current goal.
An exact proof term for the current goal is Lax n Hn .
An exact proof term for the current goal is Lxb n Hn .
We prove the intermediate
claim L1 :
∀q ∈ SNoS_ ω , q ∈ L ∨ q ∈ R .
Let q be given.
Assume Hq .
Apply dneg to the current goal.
Assume HCq : ¬ (q ∈ L ∨ q ∈ R ) .
Assume Hq1 Hq2 Hq3 Hq4 .
We prove the intermediate claim L1a : ∀w ∈ L , w < q .
Let w be given.
Assume Hw : w ∈ L .
Apply SepE (SNoS_ ω ) (λq ⇒ ∃m ∈ ω , q < a m ) w Hw to the current goal.
Assume H3 .
Apply H3 to the current goal.
Let n be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : w < a n .
Assume Hw1 Hw2 Hw3 Hw4 .
Assume H4 : w < q .
An exact proof term for the current goal is H4 .
Assume H4 : q ≤ w .
Apply HCq to the current goal.
Apply orIL to the current goal.
We will prove q ∈ L .
Apply SepI to the current goal.
An exact proof term for the current goal is Hq .
We will
prove ∃n ∈ ω , q < a n .
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn .
We will prove q < a n .
An
exact proof term for the current goal is
SNoLeLt_tra q w (a n ) Hq3 Hw3 (La1 n Hn ) H4 H3 .
We prove the intermediate claim L1b : ∀z ∈ R , q < z .
Let z be given.
Assume Hz : z ∈ R .
Apply SepE (SNoS_ ω ) (λq ⇒ ∃m ∈ ω , b m < q ) z Hz to the current goal.
Assume H3 .
Apply H3 to the current goal.
Let n be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : b n < z .
Assume Hz1 Hz2 Hz3 Hz4 .
Assume H4 : q < z .
An exact proof term for the current goal is H4 .
Assume H4 : z ≤ q .
Apply HCq to the current goal.
Apply orIR to the current goal.
We will prove q ∈ R .
Apply SepI to the current goal.
An exact proof term for the current goal is Hq .
We will
prove ∃n ∈ ω , b n < q .
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn .
We will prove b n < q .
An
exact proof term for the current goal is
SNoLtLe_tra (b n ) z q (Lb1 n Hn ) Hz3 Hq3 H3 H4 .
Apply HLR5 q Hq3 L1a L1b to the current goal.
Assume _ .
Apply HC to the current goal.
We use x to witness the existential quantifier.
Apply andI to the current goal.
Assume H3 .
An exact proof term for the current goal is H3 .
Apply H2 to the current goal.
Apply H3 to the current goal.
An exact proof term for the current goal is HLR1 .
An exact proof term for the current goal is Laxb .
Apply HC to the current goal.
We use x to witness the existential quantifier.
Apply andI to the current goal.
Apply real_I to the current goal.
An exact proof term for the current goal is HLR1 .
We prove the intermediate claim Lbd1 : x ≤ b 0 .
Assume _ _ _ .
Assume _ _ .
We will prove x < x .
Apply SNoLeLt_tra x (b 0 ) x HLR1 Hb0a HLR1 Lbd1 to the current goal.
We will prove b 0 < x .
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is Hb0b .
We prove the intermediate claim Lbd2 : a 0 ≤ x .
Assume _ _ .
Assume _ _ _ .
We will prove x < x .
Apply SNoLtLe_tra x (a 0 ) x HLR1 Ha0a HLR1 to the current goal.
We will prove x < a 0 .
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is Ha0b .
We will prove a 0 ≤ x .
An exact proof term for the current goal is Lbd2 .
Let q be given.
Assume Hq1a Hq1b Hq1c Hq1d .
Apply L1 q Hq1 to the current goal.
Assume H2 : q ∈ L .
Apply SepE (SNoS_ ω ) (λq ⇒ ∃m ∈ ω , q < a m ) q H2 to the current goal.
Assume _ H3 .
Apply H3 to the current goal.
Let n be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : q < a n .
Assume _ _ _ _ _ .
Assume _ .
We prove the intermediate claim L2 : q = a n .
Apply H4 q Hq1 to the current goal.
Let k be given.
We prove the intermediate claim L2a : 0 < a n + - q .
An
exact proof term for the current goal is
SNoLt_minus_pos q (a n ) Hq1c (La1 n Hn ) H3 .
We prove the intermediate claim L2b : a n ≤ x .
An exact proof term for the current goal is Lax n Hn .
We prove the intermediate claim L2c : 0 < x + - q .
We will prove q < x .
An
exact proof term for the current goal is
SNoLtLe_tra q (a n ) x Hq1c (La1 n Hn ) HLR1 H3 L2b .
rewrite the current goal using
abs_SNo_dist_swap q (a n ) Hq1c (La1 n Hn ) (from left to right).
rewrite the current goal using
pos_abs_SNo (a n + - q ) L2a (from left to right).
We will
prove a n + - q < eps_ k .
We will prove a n + - q ≤ x + - q .
We will prove a n ≤ x .
An exact proof term for the current goal is L2b .
We will
prove x + - q < eps_ k .
rewrite the current goal using
pos_abs_SNo (x + - q ) L2c (from right to left).
An exact proof term for the current goal is Hq2 k Hk .
rewrite the current goal using L2 (from left to right) at position 2.
An exact proof term for the current goal is H3 .
Assume H2 : q ∈ R .
Apply SepE (SNoS_ ω ) (λq ⇒ ∃m ∈ ω , b m < q ) q H2 to the current goal.
Assume _ H3 .
Apply H3 to the current goal.
Let n be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : b n < q .
Assume _ _ _ _ _ .
Assume _ .
We prove the intermediate claim L3 : q = b n .
Apply H4 q Hq1 to the current goal.
Let k be given.
We prove the intermediate claim L3a : 0 < q + - b n .
An
exact proof term for the current goal is
SNoLt_minus_pos (b n ) q (Lb1 n Hn ) Hq1c H3 .
We prove the intermediate claim L3b : x ≤ b n .
An exact proof term for the current goal is Lxb n Hn .
We prove the intermediate claim L3c : 0 < q + - x .
We will prove x < q .
An
exact proof term for the current goal is
SNoLeLt_tra x (b n ) q HLR1 (Lb1 n Hn ) Hq1c L3b H3 .
rewrite the current goal using
pos_abs_SNo (q + - b n ) L3a (from left to right).
We will
prove q + - b n < eps_ k .
We will prove q + - b n ≤ q + - x .
We will prove - b n ≤ - x .
We will
prove q + - x < eps_ k .
rewrite the current goal using
pos_abs_SNo (q + - x ) L3c (from right to left).
An exact proof term for the current goal is Hq2 k Hk .
rewrite the current goal using L3 (from left to right) at position 1.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is Laxb .
∎
Proof: Let a be given.
Assume Ha .
Let b be given.
Assume Hb .
Assume H1 .
Let n be given.
Assume Hn .
We prove the intermediate
claim L1 :
ordsucc n = n + 1 .
rewrite the current goal using
add_nat_0R (from left to right).
Use reflexivity.
rewrite the current goal using L1 (from left to right).
An exact proof term for the current goal is H1 n Hn .
∎
End of Section Reals