We prove the intermediate
claim Hf1fun0:
function_on f1 A R.
An
exact proof term for the current goal is
(andEL (function_on f1 A R) (∀a : set, a ∈ A → ∃y : set, y ∈ R ∧ (a,y) ∈ f1) Hf1_total).
We prove the intermediate
claim Hf1s_fun:
function_on f1s A R.
An
exact proof term for the current goal is
(andEL (function_on f1s A R) (∀x : set, x ∈ A → ∃y : set, y ∈ R ∧ (x,y) ∈ f1s) Hf1s_total).
Let x be given.
We prove the intermediate
claim HxR:
apply_fun f1 x ∈ R.
An exact proof term for the current goal is (Hf1fun0 x HxA).
Use reflexivity.
We prove the intermediate
claim Hf1s_I:
∀x : set, x ∈ A → apply_fun f1s x ∈ I.
Let x be given.
We prove the intermediate
claim Hf1xI2:
apply_fun f1 x ∈ I2.
An exact proof term for the current goal is (Hf1_range x HxA).
We prove the intermediate
claim Hm23R:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den H23R).
We prove the intermediate
claim Hf1xR:
apply_fun f1 x ∈ R.
We prove the intermediate
claim Hf1xS:
SNo (apply_fun f1 x).
We prove the intermediate
claim Hhi:
Rle (apply_fun f1 x) den.
We prove the intermediate
claim Hnlt_hi:
¬ (Rlt den (apply_fun f1 x)).
An exact proof term for the current goal is (Hf1s_apply x HxA).
We prove the intermediate
claim HyR:
apply_fun f1s x ∈ R.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim Hy_le_1:
Rle (apply_fun f1s x) 1.
We prove the intermediate
claim H1lty:
1 < apply_fun f1s x.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
rewrite the current goal using HyEq (from left to right) at position 1.
We prove the intermediate
claim Hden_lt_f1x:
den < apply_fun f1 x.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate
claim Hbad:
Rlt den (apply_fun f1 x).
An
exact proof term for the current goal is
(RltI den (apply_fun f1 x) H23R Hf1xR Hden_lt_f1x).
An exact proof term for the current goal is (Hnlt_hi Hbad).
rewrite the current goal using HyEq (from left to right) at position 1.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
An exact proof term for the current goal is (Hnlt_lo Hbad).
We prove the intermediate
claim HIcR:
I ⊆ R.
Set h to be the term
pair_map A f g0neg.
We prove the intermediate
claim Heq:
f1 = f1c.
Let p be given.
Let x be given.
rewrite the current goal using Hpeq (from left to right).
An
exact proof term for the current goal is
(pair_map_apply A R R f g0neg x HxA).
We prove the intermediate
claim HxTa:
x ∈ A.
An exact proof term for the current goal is HxA.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim Hg0xR:
apply_fun g0 x ∈ R.
Use reflexivity.
rewrite the current goal using Hhx (from left to right).
rewrite the current goal using Hg0negx (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hadd (from right to left).
Let p be given.
Let x be given.
rewrite the current goal using Hpeq (from left to right).
An
exact proof term for the current goal is
(pair_map_apply A R R f g0neg x HxA).
We prove the intermediate
claim Hg0xR:
apply_fun g0 x ∈ R.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
rewrite the current goal using Hhx (from left to right).
rewrite the current goal using Hg0negx (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hadd (from left to right).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hf1c_cont.
We prove the intermediate
claim HISubR:
I ⊆ R.
rewrite the current goal using HTiEq (from left to right).
Apply Hex_u1 to the current goal.
Let u1 be given.
Assume Hu1.
We prove the intermediate
claim Hu1contI0:
continuous_map X Tx I0 T0 u1.
We prove the intermediate
claim HI0subR:
I0 ⊆ R.
We prove the intermediate
claim HdenR:
den ∈ R.
We prove the intermediate
claim HdenPos:
0 < den.
Set h1 to be the term
pair_map X g0 u1s.
We prove the intermediate
claim HIcR:
I ⊆ R.
An
exact proof term for the current goal is
(add_two_continuous_R A Ta f1s u1neg HTa Hf1s_contR Hu1neg_cont).
Let x be given.
rewrite the current goal using
(pair_map_apply A R R f1s u1neg x HxA) (from left to right).
We prove the intermediate
claim Hf1sRx:
apply_fun f1s x ∈ R.
We prove the intermediate
claim Hu1negRx:
apply_fun u1neg x ∈ R.
rewrite the current goal using
(pair_map_apply A R R f1s u1neg x HxA) (from left to right).
We prove the intermediate
claim Hu1Rx:
apply_fun u1 x ∈ R.
Use reflexivity.
We prove the intermediate
claim Hr1_range:
∀x : set, x ∈ A → apply_fun r1 x ∈ I2.
Let x be given.
We prove the intermediate
claim Hf1sIx:
apply_fun f1s x ∈ I.
An exact proof term for the current goal is (Hf1s_I x HxA).
We prove the intermediate
claim HB1_cases:
x ∈ B1 ∨ ¬ (x ∈ B1).
An
exact proof term for the current goal is
(xm (x ∈ B1)).
Apply (HB1_cases (apply_fun r1 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu1_on_B1 x HxB1).
rewrite the current goal using (Hr1_apply x HxA) (from left to right).
rewrite the current goal using Hu1eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr1eq (from left to right).
We prove the intermediate
claim Hf1sI1I:
apply_fun f1s x ∈ I1 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun f1s x0 ∈ I1 ∩ I) x HxB1).
We prove the intermediate
claim Hf1sI1:
apply_fun f1s x ∈ I1.
We prove the intermediate
claim Hf1sRx:
apply_fun f1s x ∈ R.
An exact proof term for the current goal is Hlow_tmp.
An exact proof term for the current goal is Hup0_tmp.
We prove the intermediate
claim HC1_cases:
x ∈ C1 ∨ ¬ (x ∈ C1).
An
exact proof term for the current goal is
(xm (x ∈ C1)).
Apply (HC1_cases (apply_fun r1 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu1_on_C1 x HxC1).
rewrite the current goal using (Hr1_apply x HxA) (from left to right).
rewrite the current goal using Hu1eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr1eq (from left to right).
We prove the intermediate
claim Hf1sI3I:
apply_fun f1s x ∈ I3 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun f1s x0 ∈ I3 ∩ I) x HxC1).
We prove the intermediate
claim Hf1sI3:
apply_fun f1s x ∈ I3.
We prove the intermediate
claim Hf1sRx:
apply_fun f1s x ∈ R.
An exact proof term for the current goal is H0le_tmp.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim HnotI1:
¬ (apply_fun f1s x ∈ I1).
We prove the intermediate
claim Hf1sI1I:
apply_fun f1s x ∈ I1 ∩ I.
We prove the intermediate
claim HxB1':
x ∈ B1.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun f1s x0 ∈ I1 ∩ I) x HxA Hf1sI1I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotB1 HxB1').
We prove the intermediate
claim HnotI3:
¬ (apply_fun f1s x ∈ I3).
We prove the intermediate
claim Hf1sI3I:
apply_fun f1s x ∈ I3 ∩ I.
We prove the intermediate
claim HxC1':
x ∈ C1.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun f1s x0 ∈ I3 ∩ I) x HxA Hf1sI3I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotC1 HxC1').
We prove the intermediate
claim Hf1sRx:
apply_fun f1s x ∈ R.
We prove the intermediate
claim Hnlt_1_fx:
¬ (Rlt 1 (apply_fun f1s x)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_fx_m1 Hbad).
An exact proof term for the current goal is Hok.
An exact proof term for the current goal is Hok.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1_fx Hbad).
We prove the intermediate
claim Hf1sI0:
apply_fun f1s x ∈ I0.
rewrite the current goal using HI0_def (from left to right).
An exact proof term for the current goal is HxSep.
We prove the intermediate
claim Hu1funI0:
function_on u1 X I0.
We prove the intermediate
claim Hu1xI0:
apply_fun u1 x ∈ I0.
An exact proof term for the current goal is (Hu1funI0 x HxX).
We prove the intermediate
claim Hu1xR:
apply_fun u1 x ∈ R.
rewrite the current goal using (Hr1_apply x HxA) (from left to right).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is Hlow_tmp.
rewrite the current goal using Hdef23 (from left to right) at position 1.
An exact proof term for the current goal is Hup_tmp.
We prove the intermediate
claim Hr1s_cont:
continuous_map A Ta I Ti r1s.
We prove the intermediate
claim Hr1s_I:
∀x : set, x ∈ A → apply_fun r1s x ∈ I.
Let x be given.
We prove the intermediate
claim Hr1xI2:
apply_fun r1 x ∈ I2.
An exact proof term for the current goal is (Hr1_range x HxA).
We prove the intermediate
claim HmdenR:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den H23R).
We prove the intermediate
claim Hr1xR:
apply_fun r1 x ∈ R.
We prove the intermediate
claim Hr1xS:
SNo (apply_fun r1 x).
We prove the intermediate
claim Hhi:
Rle (apply_fun r1 x) den.
We prove the intermediate
claim Hnlt_hi:
¬ (Rlt den (apply_fun r1 x)).
We prove the intermediate
claim HyR:
apply_fun r1s x ∈ R.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim Hy_le_1:
Rle (apply_fun r1s x) 1.
We prove the intermediate
claim H1lty:
1 < apply_fun r1s x.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
rewrite the current goal using HyEq (from left to right) at position 1.
We prove the intermediate
claim Hden_lt_r1x:
den < apply_fun r1 x.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate
claim Hbad:
Rlt den (apply_fun r1 x).
An
exact proof term for the current goal is
(RltI den (apply_fun r1 x) H23R Hr1xR Hden_lt_r1x).
An exact proof term for the current goal is (Hnlt_hi Hbad).
rewrite the current goal using HyEq (from left to right) at position 1.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
An
exact proof term for the current goal is
(RltI (apply_fun r1 x) (minus_SNo den) Hr1xR HmdenR Hr1x_lt_mden).
An exact proof term for the current goal is (Hnlt_lo Hbad).
rewrite the current goal using HTiEq (from left to right).
Apply Hex_u2 to the current goal.
Let u2 be given.
Assume Hu2.
We prove the intermediate
claim Hu2contI0:
continuous_map X Tx I0 T0 u2.
We prove the intermediate
claim HI0subR:
I0 ⊆ R.
Set den2 to be the term
mul_SNo den den.
We prove the intermediate
claim Hden2R:
den2 ∈ R.
An
exact proof term for the current goal is
(real_mul_SNo den HdenR den HdenR).
We prove the intermediate
claim Hden2pos:
0 < den2.
An
exact proof term for the current goal is
(mul_SNo_pos_pos den den H23S H23S HdenPos HdenPos).
An
exact proof term for the current goal is
(add_two_continuous_R X Tx g1 u2s HTx Hg1cont Hu2s_cont).
An
exact proof term for the current goal is
(add_two_continuous_R A Ta r1s u2neg HTa Hr1s_contR Hu2neg_cont).
Let x be given.
rewrite the current goal using
(pair_map_apply A R R r1s u2neg x HxA) (from left to right).
We prove the intermediate
claim Hr1sRx:
apply_fun r1s x ∈ R.
We prove the intermediate
claim Hu2negRx:
apply_fun u2neg x ∈ R.
rewrite the current goal using
(pair_map_apply A R R r1s u2neg x HxA) (from left to right).
We prove the intermediate
claim Hu2Rx:
apply_fun u2 x ∈ R.
Use reflexivity.
We prove the intermediate
claim Hr2_range:
∀x : set, x ∈ A → apply_fun r2 x ∈ I2.
Let x be given.
We prove the intermediate
claim Hr1sIx:
apply_fun r1s x ∈ I.
We prove the intermediate
claim HB2_cases:
x ∈ B2 ∨ ¬ (x ∈ B2).
An
exact proof term for the current goal is
(xm (x ∈ B2)).
Apply (HB2_cases (apply_fun r2 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu2_on_B2 x HxB2).
rewrite the current goal using (Hr2_apply x HxA) (from left to right).
rewrite the current goal using Hu2eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr2eq (from left to right).
We prove the intermediate
claim Hr1sI1I:
apply_fun r1s x ∈ I1 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r1s x0 ∈ I1 ∩ I) x HxB2).
We prove the intermediate
claim Hr1sI1:
apply_fun r1s x ∈ I1.
We prove the intermediate
claim Hr1sRx:
apply_fun r1s x ∈ R.
An exact proof term for the current goal is Hlow_tmp.
An exact proof term for the current goal is Hup0_tmp.
We prove the intermediate
claim HC2_cases:
x ∈ C2 ∨ ¬ (x ∈ C2).
An
exact proof term for the current goal is
(xm (x ∈ C2)).
Apply (HC2_cases (apply_fun r2 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu2_on_C2 x HxC2).
rewrite the current goal using (Hr2_apply x HxA) (from left to right).
rewrite the current goal using Hu2eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr2eq (from left to right).
We prove the intermediate
claim Hr1sI3I:
apply_fun r1s x ∈ I3 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r1s x0 ∈ I3 ∩ I) x HxC2).
We prove the intermediate
claim Hr1sI3:
apply_fun r1s x ∈ I3.
We prove the intermediate
claim Hr1sRx:
apply_fun r1s x ∈ R.
An exact proof term for the current goal is H0le_tmp.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim HnotI1:
¬ (apply_fun r1s x ∈ I1).
We prove the intermediate
claim Hr1sI1I:
apply_fun r1s x ∈ I1 ∩ I.
We prove the intermediate
claim HxB2':
x ∈ B2.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r1s x0 ∈ I1 ∩ I) x HxA Hr1sI1I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotB2 HxB2').
We prove the intermediate
claim HnotI3:
¬ (apply_fun r1s x ∈ I3).
We prove the intermediate
claim Hr1sI3I:
apply_fun r1s x ∈ I3 ∩ I.
We prove the intermediate
claim HxC2':
x ∈ C2.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r1s x0 ∈ I3 ∩ I) x HxA Hr1sI3I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotC2 HxC2').
We prove the intermediate
claim Hr1sRx:
apply_fun r1s x ∈ R.
We prove the intermediate
claim Hnlt_1_fx:
¬ (Rlt 1 (apply_fun r1s x)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_fx_m1 Hbad).
An exact proof term for the current goal is Hok.
An exact proof term for the current goal is Hok.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1_fx Hbad).
We prove the intermediate
claim Hr1sI0:
apply_fun r1s x ∈ I0.
rewrite the current goal using HI0_def (from left to right).
An exact proof term for the current goal is HxSep.
We prove the intermediate
claim Hu2funI0:
function_on u2 X I0.
We prove the intermediate
claim Hu2xI0:
apply_fun u2 x ∈ I0.
An exact proof term for the current goal is (Hu2funI0 x HxX).
We prove the intermediate
claim Hu2xR:
apply_fun u2 x ∈ R.
rewrite the current goal using (Hr2_apply x HxA) (from left to right).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is Hlow_tmp.
rewrite the current goal using Hdef23 (from left to right).
An exact proof term for the current goal is Hup_tmp.
We prove the intermediate
claim Hr2s_cont:
continuous_map A Ta I Ti r2s.
We prove the intermediate
claim Hr2s_I:
∀x : set, x ∈ A → apply_fun r2s x ∈ I.
Let x be given.
We prove the intermediate
claim Hr2xI2:
apply_fun r2 x ∈ I2.
An exact proof term for the current goal is (Hr2_range x HxA).
We prove the intermediate
claim HmdenR:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den H23R).
We prove the intermediate
claim Hr2xR:
apply_fun r2 x ∈ R.
We prove the intermediate
claim Hr2xS:
SNo (apply_fun r2 x).
We prove the intermediate
claim Hhi:
Rle (apply_fun r2 x) den.
We prove the intermediate
claim Hnlt_hi:
¬ (Rlt den (apply_fun r2 x)).
We prove the intermediate
claim HyR:
apply_fun r2s x ∈ R.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim Hy_le_1:
Rle (apply_fun r2s x) 1.
We prove the intermediate
claim H1lty:
1 < apply_fun r2s x.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
rewrite the current goal using HyEq (from left to right) at position 1.
We prove the intermediate
claim Hden_lt_r2x:
den < apply_fun r2 x.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate
claim Hbad:
Rlt den (apply_fun r2 x).
An
exact proof term for the current goal is
(RltI den (apply_fun r2 x) H23R Hr2xR Hden_lt_r2x).
An exact proof term for the current goal is (Hnlt_hi Hbad).
rewrite the current goal using HyEq (from left to right) at position 1.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
An
exact proof term for the current goal is
(RltI (apply_fun r2 x) (minus_SNo den) Hr2xR HmdenR Hr2x_lt_mden).
An exact proof term for the current goal is (Hnlt_lo Hbad).
Apply Hex_u3 to the current goal.
Let u3 be given.
Assume Hu3.
We prove the intermediate
claim Hu3contI0:
continuous_map X Tx I0 T0 u3.
We prove the intermediate
claim HI0subR:
I0 ⊆ R.
Set den3 to be the term
mul_SNo den2 den.
We prove the intermediate
claim Hden3R:
den3 ∈ R.
An
exact proof term for the current goal is
(real_mul_SNo den2 Hden2R den HdenR).
We prove the intermediate
claim Hden3pos:
0 < den3.
We prove the intermediate
claim Hden2S:
SNo den2.
An
exact proof term for the current goal is
(real_SNo den2 Hden2R).
An
exact proof term for the current goal is
(mul_SNo_pos_pos den2 den Hden2S H23S Hden2pos HdenPos).
An
exact proof term for the current goal is
(add_two_continuous_R X Tx g2 u3s HTx Hg2cont Hu3s_cont).
An
exact proof term for the current goal is
(add_two_continuous_R A Ta r2s u3neg HTa Hr2s_contR Hu3neg_cont).
Let x be given.
rewrite the current goal using
(pair_map_apply A R R r2s u3neg x HxA) (from left to right).
We prove the intermediate
claim Hr2sRx:
apply_fun r2s x ∈ R.
We prove the intermediate
claim Hu3negRx:
apply_fun u3neg x ∈ R.
rewrite the current goal using
(pair_map_apply A R R r2s u3neg x HxA) (from left to right).
We prove the intermediate
claim Hu3Rx:
apply_fun u3 x ∈ R.
Use reflexivity.
We prove the intermediate
claim Hr3_range:
∀x : set, x ∈ A → apply_fun r3 x ∈ I2.
Let x be given.
We prove the intermediate
claim Hr2sIx:
apply_fun r2s x ∈ I.
We prove the intermediate
claim HB3_cases:
x ∈ B3 ∨ ¬ (x ∈ B3).
An
exact proof term for the current goal is
(xm (x ∈ B3)).
Apply (HB3_cases (apply_fun r3 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu3_on_B3 x HxB3).
rewrite the current goal using (Hr3_apply x HxA) (from left to right).
rewrite the current goal using Hu3eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr3eq (from left to right).
We prove the intermediate
claim Hr2sI1I:
apply_fun r2s x ∈ I1 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r2s x0 ∈ I1 ∩ I) x HxB3).
We prove the intermediate
claim Hr2sI1:
apply_fun r2s x ∈ I1.
We prove the intermediate
claim Hr2sRx:
apply_fun r2s x ∈ R.
An exact proof term for the current goal is Hlow_tmp.
An exact proof term for the current goal is Hup0_tmp.
We prove the intermediate
claim HC3_cases:
x ∈ C3 ∨ ¬ (x ∈ C3).
An
exact proof term for the current goal is
(xm (x ∈ C3)).
Apply (HC3_cases (apply_fun r3 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu3_on_C3 x HxC3).
rewrite the current goal using (Hr3_apply x HxA) (from left to right).
rewrite the current goal using Hu3eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr3eq (from left to right).
We prove the intermediate
claim Hr2sI3I:
apply_fun r2s x ∈ I3 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r2s x0 ∈ I3 ∩ I) x HxC3).
We prove the intermediate
claim Hr2sI3:
apply_fun r2s x ∈ I3.
We prove the intermediate
claim Hr2sRx:
apply_fun r2s x ∈ R.
An exact proof term for the current goal is H0le_tmp.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim HnotI1:
¬ (apply_fun r2s x ∈ I1).
We prove the intermediate
claim Hr2sI1I:
apply_fun r2s x ∈ I1 ∩ I.
We prove the intermediate
claim HxB3':
x ∈ B3.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r2s x0 ∈ I1 ∩ I) x HxA Hr2sI1I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotB3 HxB3').
We prove the intermediate
claim HnotI3:
¬ (apply_fun r2s x ∈ I3).
We prove the intermediate
claim Hr2sI3I:
apply_fun r2s x ∈ I3 ∩ I.
We prove the intermediate
claim HxC3':
x ∈ C3.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r2s x0 ∈ I3 ∩ I) x HxA Hr2sI3I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotC3 HxC3').
We prove the intermediate
claim Hr2sRx:
apply_fun r2s x ∈ R.
We prove the intermediate
claim Hnlt_1_fx:
¬ (Rlt 1 (apply_fun r2s x)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_fx_m1 Hbad).
An exact proof term for the current goal is Hok.
An exact proof term for the current goal is Hok.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1_fx Hbad).
We prove the intermediate
claim Hr2sI0:
apply_fun r2s x ∈ I0.
rewrite the current goal using HI0_def (from left to right).
An exact proof term for the current goal is HxSep.
We prove the intermediate
claim Hu3funI0:
function_on u3 X I0.
We prove the intermediate
claim Hu3xI0:
apply_fun u3 x ∈ I0.
An exact proof term for the current goal is (Hu3funI0 x HxX).
We prove the intermediate
claim Hu3xR:
apply_fun u3 x ∈ R.
rewrite the current goal using (Hr3_apply x HxA) (from left to right).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is Hlow_tmp.
rewrite the current goal using Hdef23 (from left to right) at position 1.
An exact proof term for the current goal is Hup_tmp.
We prove the intermediate
claim Hr3s_cont:
continuous_map A Ta I Ti r3s.
We prove the intermediate
claim Hr3s_I:
∀x : set, x ∈ A → apply_fun r3s x ∈ I.
Let x be given.
We prove the intermediate
claim Hr3xI2:
apply_fun r3 x ∈ I2.
An exact proof term for the current goal is (Hr3_range x HxA).
We prove the intermediate
claim HmdenR:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den H23R).
We prove the intermediate
claim Hr3xR:
apply_fun r3 x ∈ R.
We prove the intermediate
claim Hr3xS:
SNo (apply_fun r3 x).
We prove the intermediate
claim Hhi:
Rle (apply_fun r3 x) den.
We prove the intermediate
claim Hnlt_hi:
¬ (Rlt den (apply_fun r3 x)).
We prove the intermediate
claim HyR:
apply_fun r3s x ∈ R.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim Hy_le_1:
Rle (apply_fun r3s x) 1.
We prove the intermediate
claim H1lty:
1 < apply_fun r3s x.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
rewrite the current goal using HyEq (from left to right) at position 1.
We prove the intermediate
claim Hden_lt_r3x:
den < apply_fun r3 x.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate
claim Hbad:
Rlt den (apply_fun r3 x).
An
exact proof term for the current goal is
(RltI den (apply_fun r3 x) H23R Hr3xR Hden_lt_r3x).
An exact proof term for the current goal is (Hnlt_hi Hbad).
rewrite the current goal using HyEq (from left to right) at position 1.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
An
exact proof term for the current goal is
(RltI (apply_fun r3 x) (minus_SNo den) Hr3xR HmdenR Hr3x_lt_mden).
An exact proof term for the current goal is (Hnlt_lo Hbad).
Apply Hex_u4 to the current goal.
Let u4 be given.
Assume Hu4.
We prove the intermediate
claim Hu4contI0:
continuous_map X Tx I0 T0 u4.
We prove the intermediate
claim HI0subR:
I0 ⊆ R.
Set den4 to be the term
mul_SNo den3 den.
We prove the intermediate
claim Hden4R:
den4 ∈ R.
An
exact proof term for the current goal is
(real_mul_SNo den3 Hden3R den H23R).
We prove the intermediate
claim Hden4pos:
0 < den4.
We prove the intermediate
claim Hden3S:
SNo den3.
An
exact proof term for the current goal is
(real_SNo den3 Hden3R).
An
exact proof term for the current goal is
(mul_SNo_pos_pos den3 den Hden3S H23S Hden3pos HdenPos).
An
exact proof term for the current goal is
(add_two_continuous_R X Tx g3 u4s HTx Hg3cont Hu4s_cont).
An
exact proof term for the current goal is
(add_two_continuous_R A Ta r3s u4neg HTa Hr3s_contR Hu4neg_cont).
Let x be given.
rewrite the current goal using
(pair_map_apply A R R r3s u4neg x HxA) (from left to right).
We prove the intermediate
claim Hr3sxI:
apply_fun r3s x ∈ I.
We prove the intermediate
claim Hr3sxR:
apply_fun r3s x ∈ R.
An
exact proof term for the current goal is
(HIcR (apply_fun r3s x) Hr3sxI).
We prove the intermediate
claim Hu4negRx:
apply_fun u4neg x ∈ R.
rewrite the current goal using
(pair_map_apply A R R r3s u4neg x HxA) (from left to right).
We prove the intermediate
claim Hu4Rx:
apply_fun u4 x ∈ R.
Use reflexivity.
We prove the intermediate
claim Hr4_range:
∀x : set, x ∈ A → apply_fun r4 x ∈ I2.
Let x be given.
We prove the intermediate
claim Hr3sIx:
apply_fun r3s x ∈ I.
We prove the intermediate
claim HB4_cases:
x ∈ B4 ∨ ¬ (x ∈ B4).
An
exact proof term for the current goal is
(xm (x ∈ B4)).
Apply (HB4_cases (apply_fun r4 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu4_on_B4 x HxB4).
rewrite the current goal using (Hr4_apply x HxA) (from left to right).
rewrite the current goal using Hu4eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr4eq (from left to right).
We prove the intermediate
claim Hr3sI1I:
apply_fun r3s x ∈ I1 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r3s x0 ∈ I1 ∩ I) x HxB4).
We prove the intermediate
claim Hr3sI1:
apply_fun r3s x ∈ I1.
We prove the intermediate
claim Hr3sRx:
apply_fun r3s x ∈ R.
An exact proof term for the current goal is Hlow_tmp.
An exact proof term for the current goal is Hup0_tmp.
We prove the intermediate
claim HC4_cases:
x ∈ C4 ∨ ¬ (x ∈ C4).
An
exact proof term for the current goal is
(xm (x ∈ C4)).
Apply (HC4_cases (apply_fun r4 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu4_on_C4 x HxC4).
rewrite the current goal using (Hr4_apply x HxA) (from left to right).
rewrite the current goal using Hu4eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr4eq (from left to right).
We prove the intermediate
claim Hr3sI3I:
apply_fun r3s x ∈ I3 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r3s x0 ∈ I3 ∩ I) x HxC4).
We prove the intermediate
claim Hr3sI3:
apply_fun r3s x ∈ I3.
We prove the intermediate
claim Hr3sRx:
apply_fun r3s x ∈ R.
An exact proof term for the current goal is H0le_tmp.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim HnotI1:
¬ (apply_fun r3s x ∈ I1).
We prove the intermediate
claim Hr3sI1I:
apply_fun r3s x ∈ I1 ∩ I.
We prove the intermediate
claim HxB4':
x ∈ B4.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r3s x0 ∈ I1 ∩ I) x HxA Hr3sI1I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotB4 HxB4').
We prove the intermediate
claim HnotI3:
¬ (apply_fun r3s x ∈ I3).
We prove the intermediate
claim Hr3sI3I:
apply_fun r3s x ∈ I3 ∩ I.
We prove the intermediate
claim HxC4':
x ∈ C4.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r3s x0 ∈ I3 ∩ I) x HxA Hr3sI3I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotC4 HxC4').
We prove the intermediate
claim Hr3sRx:
apply_fun r3s x ∈ R.
We prove the intermediate
claim Hnlt_1_fx:
¬ (Rlt 1 (apply_fun r3s x)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_fx_m1 Hbad).
An exact proof term for the current goal is Hok.
An exact proof term for the current goal is Hok.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1_fx Hbad).
We prove the intermediate
claim Hr3sI0:
apply_fun r3s x ∈ I0.
rewrite the current goal using HI0_def (from left to right).
An exact proof term for the current goal is HxSep.
We prove the intermediate
claim Hu4funI0:
function_on u4 X I0.
We prove the intermediate
claim Hu4xI0:
apply_fun u4 x ∈ I0.
An exact proof term for the current goal is (Hu4funI0 x HxX).
We prove the intermediate
claim Hu4xR:
apply_fun u4 x ∈ R.
rewrite the current goal using (Hr4_apply x HxA) (from left to right).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is Hlow_tmp.
rewrite the current goal using Hdef23 (from left to right) at position 1.
An exact proof term for the current goal is Hup_tmp.
We prove the intermediate
claim Hr4s_cont:
continuous_map A Ta I Ti r4s.
We prove the intermediate
claim Hr4s_I:
∀x : set, x ∈ A → apply_fun r4s x ∈ I.
Let x be given.
We prove the intermediate
claim Hr4xI2:
apply_fun r4 x ∈ I2.
An exact proof term for the current goal is (Hr4_range x HxA).
We prove the intermediate
claim HmdenR:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den H23R).
We prove the intermediate
claim Hr4xR:
apply_fun r4 x ∈ R.
We prove the intermediate
claim Hr4xS:
SNo (apply_fun r4 x).
We prove the intermediate
claim Hhi:
Rle (apply_fun r4 x) den.
We prove the intermediate
claim Hnlt_hi:
¬ (Rlt den (apply_fun r4 x)).
We prove the intermediate
claim HyR:
apply_fun r4s x ∈ R.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim Hy_le_1:
Rle (apply_fun r4s x) 1.
We prove the intermediate
claim H1lty:
1 < apply_fun r4s x.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
rewrite the current goal using HyEq (from left to right) at position 1.
We prove the intermediate
claim Hden_lt_r4x:
den < apply_fun r4 x.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate
claim Hbad:
Rlt den (apply_fun r4 x).
An
exact proof term for the current goal is
(RltI den (apply_fun r4 x) H23R Hr4xR Hden_lt_r4x).
An exact proof term for the current goal is (Hnlt_hi Hbad).
rewrite the current goal using HyEq (from left to right) at position 1.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
An
exact proof term for the current goal is
(RltI (apply_fun r4 x) (minus_SNo den) Hr4xR HmdenR Hr4x_lt_mden).
An exact proof term for the current goal is (Hnlt_lo Hbad).
Apply Hex_u5 to the current goal.
Let u5 be given.
Assume Hu5.
We prove the intermediate
claim Hu5contI0:
continuous_map X Tx I0 T0 u5.
We prove the intermediate
claim HI0subR:
I0 ⊆ R.
Set den5 to be the term
mul_SNo den4 den.
We prove the intermediate
claim Hden5R:
den5 ∈ R.
An
exact proof term for the current goal is
(real_mul_SNo den4 Hden4R den H23R).
We prove the intermediate
claim Hden5pos:
0 < den5.
We prove the intermediate
claim Hden4S:
SNo den4.
An
exact proof term for the current goal is
(real_SNo den4 Hden4R).
An
exact proof term for the current goal is
(mul_SNo_pos_pos den4 den Hden4S H23S Hden4pos HdenPos).
An
exact proof term for the current goal is
(add_two_continuous_R X Tx g4 u5s HTx Hg4cont Hu5s_cont).
An
exact proof term for the current goal is
(add_two_continuous_R A Ta r4s u5neg HTa Hr4s_contR Hu5neg_cont).
Let x be given.
rewrite the current goal using
(pair_map_apply A R R r4s u5neg x HxA) (from left to right).
We prove the intermediate
claim Hr4sxI:
apply_fun r4s x ∈ I.
We prove the intermediate
claim Hr4sxR:
apply_fun r4s x ∈ R.
An
exact proof term for the current goal is
(HIcR (apply_fun r4s x) Hr4sxI).
We prove the intermediate
claim Hu5negRx:
apply_fun u5neg x ∈ R.
rewrite the current goal using
(pair_map_apply A R R r4s u5neg x HxA) (from left to right).
We prove the intermediate
claim Hu5Rx:
apply_fun u5 x ∈ R.
Use reflexivity.
We prove the intermediate
claim Hr5_range:
∀x : set, x ∈ A → apply_fun r5 x ∈ I2.
Let x be given.
We prove the intermediate
claim Hr4sIx:
apply_fun r4s x ∈ I.
We prove the intermediate
claim HB5_cases:
x ∈ B5 ∨ ¬ (x ∈ B5).
An
exact proof term for the current goal is
(xm (x ∈ B5)).
Apply (HB5_cases (apply_fun r5 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu5_on_B5 x HxB5).
rewrite the current goal using (Hr5_apply x HxA) (from left to right).
rewrite the current goal using Hu5eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr5eq (from left to right).
We prove the intermediate
claim Hr4sI1I:
apply_fun r4s x ∈ I1 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r4s x0 ∈ I1 ∩ I) x HxB5).
We prove the intermediate
claim Hr4sI1:
apply_fun r4s x ∈ I1.
We prove the intermediate
claim Hr4sRx:
apply_fun r4s x ∈ R.
An exact proof term for the current goal is Hlow_tmp.
An exact proof term for the current goal is Hup0_tmp.
We prove the intermediate
claim HC5_cases:
x ∈ C5 ∨ ¬ (x ∈ C5).
An
exact proof term for the current goal is
(xm (x ∈ C5)).
Apply (HC5_cases (apply_fun r5 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu5_on_C5 x HxC5).
rewrite the current goal using (Hr5_apply x HxA) (from left to right).
rewrite the current goal using Hu5eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr5eq (from left to right).
We prove the intermediate
claim Hr4sI3I:
apply_fun r4s x ∈ I3 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r4s x0 ∈ I3 ∩ I) x HxC5).
We prove the intermediate
claim Hr4sI3:
apply_fun r4s x ∈ I3.
We prove the intermediate
claim Hr4sRx:
apply_fun r4s x ∈ R.
An exact proof term for the current goal is H0le_tmp.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim HnotI1:
¬ (apply_fun r4s x ∈ I1).
We prove the intermediate
claim Hr4sI1I:
apply_fun r4s x ∈ I1 ∩ I.
We prove the intermediate
claim HxB5':
x ∈ B5.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r4s x0 ∈ I1 ∩ I) x HxA Hr4sI1I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotB5 HxB5').
We prove the intermediate
claim HnotI3:
¬ (apply_fun r4s x ∈ I3).
We prove the intermediate
claim Hr4sI3I:
apply_fun r4s x ∈ I3 ∩ I.
We prove the intermediate
claim HxC5':
x ∈ C5.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r4s x0 ∈ I3 ∩ I) x HxA Hr4sI3I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotC5 HxC5').
We prove the intermediate
claim Hr4sRx:
apply_fun r4s x ∈ R.
We prove the intermediate
claim Hnlt_1_fx:
¬ (Rlt 1 (apply_fun r4s x)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_fx_m1 Hbad).
An exact proof term for the current goal is Hok.
An exact proof term for the current goal is Hok.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1_fx Hbad).
We prove the intermediate
claim Hr4sI0:
apply_fun r4s x ∈ I0.
rewrite the current goal using HI0_def (from left to right).
An exact proof term for the current goal is HxSep.
We prove the intermediate
claim Hu5funI0:
function_on u5 X I0.
We prove the intermediate
claim Hu5xI0:
apply_fun u5 x ∈ I0.
An exact proof term for the current goal is (Hu5funI0 x HxX).
We prove the intermediate
claim Hu5xR:
apply_fun u5 x ∈ R.
rewrite the current goal using (Hr5_apply x HxA) (from left to right).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is Hlow_tmp.
rewrite the current goal using Hdef23 (from left to right) at position 1.
An exact proof term for the current goal is Hup_tmp.
We prove the intermediate
claim Hr5s_cont:
continuous_map A Ta I Ti r5s.
We prove the intermediate
claim Hr5s_I:
∀x : set, x ∈ A → apply_fun r5s x ∈ I.
Let x be given.
We prove the intermediate
claim Hr5xI2:
apply_fun r5 x ∈ I2.
An exact proof term for the current goal is (Hr5_range x HxA).
We prove the intermediate
claim HmdenR:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den H23R).
We prove the intermediate
claim Hr5xR:
apply_fun r5 x ∈ R.
We prove the intermediate
claim Hr5xS:
SNo (apply_fun r5 x).
We prove the intermediate
claim Hhi:
Rle (apply_fun r5 x) den.
We prove the intermediate
claim Hnlt_hi:
¬ (Rlt den (apply_fun r5 x)).
We prove the intermediate
claim HyR:
apply_fun r5s x ∈ R.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim Hy_le_1:
Rle (apply_fun r5s x) 1.
We prove the intermediate
claim H1lty:
1 < apply_fun r5s x.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
rewrite the current goal using HyEq (from left to right) at position 1.
We prove the intermediate
claim Hden_lt_r5x:
den < apply_fun r5 x.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate
claim Hbad:
Rlt den (apply_fun r5 x).
An
exact proof term for the current goal is
(RltI den (apply_fun r5 x) H23R Hr5xR Hden_lt_r5x).
An exact proof term for the current goal is (Hnlt_hi Hbad).
rewrite the current goal using HyEq (from left to right) at position 1.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
An
exact proof term for the current goal is
(RltI (apply_fun r5 x) (minus_SNo den) Hr5xR HmdenR Hr5x_lt_mden).
An exact proof term for the current goal is (Hnlt_lo Hbad).
Apply Hex_u6 to the current goal.
Let u6 be given.
Assume Hu6.
We prove the intermediate
claim Hu6contI0:
continuous_map X Tx I0 T0 u6.
We prove the intermediate
claim HI0subR:
I0 ⊆ R.
Set den6 to be the term
mul_SNo den5 den.
We prove the intermediate
claim Hden6R:
den6 ∈ R.
An
exact proof term for the current goal is
(real_mul_SNo den5 Hden5R den H23R).
We prove the intermediate
claim Hden6pos:
0 < den6.
We prove the intermediate
claim Hden5S:
SNo den5.
An
exact proof term for the current goal is
(real_SNo den5 Hden5R).
An
exact proof term for the current goal is
(mul_SNo_pos_pos den5 den Hden5S H23S Hden5pos HdenPos).
An
exact proof term for the current goal is
(add_two_continuous_R X Tx g5 u6s HTx Hg5cont Hu6s_cont).
An
exact proof term for the current goal is
(add_two_continuous_R A Ta r5s u6neg HTa Hr5s_contR Hu6neg_cont).
Let x be given.
rewrite the current goal using
(pair_map_apply A R R r5s u6neg x HxA) (from left to right).
We prove the intermediate
claim Hr5sxI:
apply_fun r5s x ∈ I.
We prove the intermediate
claim Hr5sxR:
apply_fun r5s x ∈ R.
An
exact proof term for the current goal is
(HIcR (apply_fun r5s x) Hr5sxI).
We prove the intermediate
claim Hu6negRx:
apply_fun u6neg x ∈ R.
rewrite the current goal using
(pair_map_apply A R R r5s u6neg x HxA) (from left to right).
We prove the intermediate
claim Hu6Rx:
apply_fun u6 x ∈ R.
Use reflexivity.
We prove the intermediate
claim Hr6_range:
∀x : set, x ∈ A → apply_fun r6 x ∈ I2.
Let x be given.
We prove the intermediate
claim Hr5sIx:
apply_fun r5s x ∈ I.
We prove the intermediate
claim HB6_cases:
x ∈ B6 ∨ ¬ (x ∈ B6).
An
exact proof term for the current goal is
(xm (x ∈ B6)).
Apply (HB6_cases (apply_fun r6 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu6_on_B6 x HxB6).
rewrite the current goal using (Hr6_apply x HxA) (from left to right).
rewrite the current goal using Hu6eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr6eq (from left to right).
We prove the intermediate
claim Hr5sI1I:
apply_fun r5s x ∈ I1 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r5s x0 ∈ I1 ∩ I) x HxB6).
We prove the intermediate
claim Hr5sI1:
apply_fun r5s x ∈ I1.
We prove the intermediate
claim Hr5sRx:
apply_fun r5s x ∈ R.
An exact proof term for the current goal is Hlow_tmp.
An exact proof term for the current goal is Hup0_tmp.
We prove the intermediate
claim HC6_cases:
x ∈ C6 ∨ ¬ (x ∈ C6).
An
exact proof term for the current goal is
(xm (x ∈ C6)).
Apply (HC6_cases (apply_fun r6 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu6_on_C6 x HxC6).
rewrite the current goal using (Hr6_apply x HxA) (from left to right).
rewrite the current goal using Hu6eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr6eq (from left to right).
We prove the intermediate
claim Hr5sI3I:
apply_fun r5s x ∈ I3 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r5s x0 ∈ I3 ∩ I) x HxC6).
We prove the intermediate
claim Hr5sI3:
apply_fun r5s x ∈ I3.
We prove the intermediate
claim Hr5sRx:
apply_fun r5s x ∈ R.
An exact proof term for the current goal is H0le_tmp.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim HnotI1:
¬ (apply_fun r5s x ∈ I1).
We prove the intermediate
claim Hr5sI1I:
apply_fun r5s x ∈ I1 ∩ I.
We prove the intermediate
claim HxB6':
x ∈ B6.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r5s x0 ∈ I1 ∩ I) x HxA Hr5sI1I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotB6 HxB6').
We prove the intermediate
claim HnotI3:
¬ (apply_fun r5s x ∈ I3).
We prove the intermediate
claim Hr5sI3I:
apply_fun r5s x ∈ I3 ∩ I.
We prove the intermediate
claim HxC6':
x ∈ C6.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r5s x0 ∈ I3 ∩ I) x HxA Hr5sI3I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotC6 HxC6').
We prove the intermediate
claim Hr5sRx:
apply_fun r5s x ∈ R.
We prove the intermediate
claim Hnlt_1_fx:
¬ (Rlt 1 (apply_fun r5s x)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_fx_m1 Hbad).
An exact proof term for the current goal is Hok.
An exact proof term for the current goal is Hok.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1_fx Hbad).
We prove the intermediate
claim Hr5sI0:
apply_fun r5s x ∈ I0.
rewrite the current goal using HI0_def (from left to right).
An exact proof term for the current goal is HxSep.
We prove the intermediate
claim Hu6funI0:
function_on u6 X I0.
We prove the intermediate
claim Hu6xI0:
apply_fun u6 x ∈ I0.
An exact proof term for the current goal is (Hu6funI0 x HxX).
We prove the intermediate
claim Hu6xR:
apply_fun u6 x ∈ R.
rewrite the current goal using (Hr6_apply x HxA) (from left to right).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is Hlow_tmp.
rewrite the current goal using Hdef23 (from left to right) at position 1.
An exact proof term for the current goal is Hup_tmp.
We prove the intermediate
claim Hr6s_cont:
continuous_map A Ta I Ti r6s.
We prove the intermediate
claim Hr6s_I:
∀x : set, x ∈ A → apply_fun r6s x ∈ I.
Let x be given.
We prove the intermediate
claim Hr6xI2:
apply_fun r6 x ∈ I2.
An exact proof term for the current goal is (Hr6_range x HxA).
We prove the intermediate
claim HmdenR:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den H23R).
We prove the intermediate
claim Hr6xR:
apply_fun r6 x ∈ R.
We prove the intermediate
claim Hr6xS:
SNo (apply_fun r6 x).
We prove the intermediate
claim Hhi:
Rle (apply_fun r6 x) den.
We prove the intermediate
claim Hnlt_hi:
¬ (Rlt den (apply_fun r6 x)).
We prove the intermediate
claim HyR:
apply_fun r6s x ∈ R.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim Hy_le_1:
Rle (apply_fun r6s x) 1.
We prove the intermediate
claim H1lty:
1 < apply_fun r6s x.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
rewrite the current goal using HyEq (from left to right) at position 1.
We prove the intermediate
claim Hden_lt_r6x:
den < apply_fun r6 x.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate
claim Hbad:
Rlt den (apply_fun r6 x).
An
exact proof term for the current goal is
(RltI den (apply_fun r6 x) H23R Hr6xR Hden_lt_r6x).
An exact proof term for the current goal is (Hnlt_hi Hbad).
rewrite the current goal using HyEq (from left to right) at position 1.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
An
exact proof term for the current goal is
(RltI (apply_fun r6 x) (minus_SNo den) Hr6xR HmdenR Hr6x_lt_mden).
An exact proof term for the current goal is (Hnlt_lo Hbad).
Apply Hex_u7 to the current goal.
Let u7 be given.
Assume Hu7.
We prove the intermediate
claim Hu7contI0:
continuous_map X Tx I0 T0 u7.
We prove the intermediate
claim HI0subR:
I0 ⊆ R.
Set den7 to be the term
mul_SNo den6 den.
We prove the intermediate
claim Hden7R:
den7 ∈ R.
An
exact proof term for the current goal is
(real_mul_SNo den6 Hden6R den H23R).
We prove the intermediate
claim Hden7pos:
0 < den7.
We prove the intermediate
claim Hden6S:
SNo den6.
An
exact proof term for the current goal is
(real_SNo den6 Hden6R).
An
exact proof term for the current goal is
(mul_SNo_pos_pos den6 den Hden6S H23S Hden6pos HdenPos).
An
exact proof term for the current goal is
(add_two_continuous_R X Tx g6 u7s HTx Hg6cont Hu7s_cont).
An
exact proof term for the current goal is
(add_two_continuous_R A Ta r6s u7neg HTa Hr6s_contR Hu7neg_cont).
Let x be given.
rewrite the current goal using
(pair_map_apply A R R r6s u7neg x HxA) (from left to right).
We prove the intermediate
claim Hr6sxI:
apply_fun r6s x ∈ I.
We prove the intermediate
claim Hr6sxR:
apply_fun r6s x ∈ R.
An
exact proof term for the current goal is
(HIcR (apply_fun r6s x) Hr6sxI).
We prove the intermediate
claim Hu7negRx:
apply_fun u7neg x ∈ R.
rewrite the current goal using
(pair_map_apply A R R r6s u7neg x HxA) (from left to right).
We prove the intermediate
claim Hu7Rx:
apply_fun u7 x ∈ R.
Use reflexivity.
We prove the intermediate
claim Hr7_range:
∀x : set, x ∈ A → apply_fun r7 x ∈ I2.
Let x be given.
We prove the intermediate
claim Hr6sIx:
apply_fun r6s x ∈ I.
We prove the intermediate
claim HB7_cases:
x ∈ B7 ∨ ¬ (x ∈ B7).
An
exact proof term for the current goal is
(xm (x ∈ B7)).
Apply (HB7_cases (apply_fun r7 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu7_on_B7 x HxB7).
rewrite the current goal using (Hr7_apply x HxA) (from left to right).
rewrite the current goal using Hu7eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr7eq (from left to right).
We prove the intermediate
claim Hr6sI1I:
apply_fun r6s x ∈ I1 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r6s x0 ∈ I1 ∩ I) x HxB7).
We prove the intermediate
claim Hr6sI1:
apply_fun r6s x ∈ I1.
We prove the intermediate
claim Hr6sRx:
apply_fun r6s x ∈ R.
An exact proof term for the current goal is Hlow_tmp.
An exact proof term for the current goal is Hup0_tmp.
We prove the intermediate
claim HC7_cases:
x ∈ C7 ∨ ¬ (x ∈ C7).
An
exact proof term for the current goal is
(xm (x ∈ C7)).
Apply (HC7_cases (apply_fun r7 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu7_on_C7 x HxC7).
rewrite the current goal using (Hr7_apply x HxA) (from left to right).
rewrite the current goal using Hu7eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr7eq (from left to right).
We prove the intermediate
claim Hr6sI3I:
apply_fun r6s x ∈ I3 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r6s x0 ∈ I3 ∩ I) x HxC7).
We prove the intermediate
claim Hr6sI3:
apply_fun r6s x ∈ I3.
We prove the intermediate
claim Hr6sRx:
apply_fun r6s x ∈ R.
An exact proof term for the current goal is H0le_tmp.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim HnotI1:
¬ (apply_fun r6s x ∈ I1).
We prove the intermediate
claim Hr6sI1I:
apply_fun r6s x ∈ I1 ∩ I.
We prove the intermediate
claim HxB7':
x ∈ B7.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r6s x0 ∈ I1 ∩ I) x HxA Hr6sI1I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotB7 HxB7').
We prove the intermediate
claim HnotI3:
¬ (apply_fun r6s x ∈ I3).
We prove the intermediate
claim Hr6sI3I:
apply_fun r6s x ∈ I3 ∩ I.
We prove the intermediate
claim HxC7':
x ∈ C7.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r6s x0 ∈ I3 ∩ I) x HxA Hr6sI3I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotC7 HxC7').
We prove the intermediate
claim Hr6sRx:
apply_fun r6s x ∈ R.
We prove the intermediate
claim Hnlt_1_fx:
¬ (Rlt 1 (apply_fun r6s x)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_fx_m1 Hbad).
An exact proof term for the current goal is Hok.
An exact proof term for the current goal is Hok.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1_fx Hbad).
We prove the intermediate
claim Hr6sI0:
apply_fun r6s x ∈ I0.
rewrite the current goal using HI0_def (from left to right).
An exact proof term for the current goal is HxSep.
We prove the intermediate
claim Hu7contI0:
continuous_map X Tx I0 T0 u7.
We prove the intermediate
claim Hu7funI0:
function_on u7 X I0.
We prove the intermediate
claim Hu7xI0:
apply_fun u7 x ∈ I0.
An exact proof term for the current goal is (Hu7funI0 x HxX).
We prove the intermediate
claim Hu7xR:
apply_fun u7 x ∈ R.
rewrite the current goal using (Hr7_apply x HxA) (from left to right).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is Hlow_tmp.
rewrite the current goal using Hdef23 (from left to right) at position 1.
An exact proof term for the current goal is Hup_tmp.
We prove the intermediate
claim Hr7s_cont:
continuous_map A Ta I Ti r7s.
We prove the intermediate
claim Hr7s_I:
∀x : set, x ∈ A → apply_fun r7s x ∈ I.
Let x be given.
We prove the intermediate
claim Hr7xI2:
apply_fun r7 x ∈ I2.
An exact proof term for the current goal is (Hr7_range x HxA).
We prove the intermediate
claim HmdenR:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den H23R).
We prove the intermediate
claim Hr7xR:
apply_fun r7 x ∈ R.
We prove the intermediate
claim Hr7xS:
SNo (apply_fun r7 x).
We prove the intermediate
claim Hhi:
Rle (apply_fun r7 x) den.
We prove the intermediate
claim Hnlt_hi:
¬ (Rlt den (apply_fun r7 x)).
We prove the intermediate
claim HyR:
apply_fun r7s x ∈ R.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim Hy_le_1:
Rle (apply_fun r7s x) 1.
We prove the intermediate
claim H1lty:
1 < apply_fun r7s x.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
rewrite the current goal using HyEq (from left to right) at position 1.
We prove the intermediate
claim Hden_lt_r7x:
den < apply_fun r7 x.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate
claim Hbad:
Rlt den (apply_fun r7 x).
An
exact proof term for the current goal is
(RltI den (apply_fun r7 x) H23R Hr7xR Hden_lt_r7x).
An exact proof term for the current goal is (Hnlt_hi Hbad).
rewrite the current goal using HyEq (from left to right) at position 1.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
An
exact proof term for the current goal is
(RltI (apply_fun r7 x) (minus_SNo den) Hr7xR HmdenR Hr7x_lt_mden).
An exact proof term for the current goal is (Hnlt_lo Hbad).
Apply Hex_u8 to the current goal.
Let u8 be given.
Assume Hu8.
We prove the intermediate
claim Hu8contI0:
continuous_map X Tx I0 T0 u8.
We prove the intermediate
claim HI0subR:
I0 ⊆ R.
Set den8 to be the term
mul_SNo den7 den.
We prove the intermediate
claim Hden8R:
den8 ∈ R.
An
exact proof term for the current goal is
(real_mul_SNo den7 Hden7R den H23R).
We prove the intermediate
claim Hden8pos:
0 < den8.
We prove the intermediate
claim Hden7S:
SNo den7.
An
exact proof term for the current goal is
(real_SNo den7 Hden7R).
An
exact proof term for the current goal is
(mul_SNo_pos_pos den7 den Hden7S H23S Hden7pos HdenPos).
An
exact proof term for the current goal is
(add_two_continuous_R X Tx g7 u8s HTx Hg7cont Hu8s_cont).
An
exact proof term for the current goal is
(add_two_continuous_R A Ta r7s u8neg HTa Hr7s_contR Hu8neg_cont).
Let x be given.
rewrite the current goal using
(pair_map_apply A R R r7s u8neg x HxA) (from left to right).
We prove the intermediate
claim Hr7sxI:
apply_fun r7s x ∈ I.
We prove the intermediate
claim Hr7sxR:
apply_fun r7s x ∈ R.
An
exact proof term for the current goal is
(HIcR (apply_fun r7s x) Hr7sxI).
We prove the intermediate
claim Hu8negRx:
apply_fun u8neg x ∈ R.
rewrite the current goal using
(pair_map_apply A R R r7s u8neg x HxA) (from left to right).
We prove the intermediate
claim Hu8Rx:
apply_fun u8 x ∈ R.
Use reflexivity.
We prove the intermediate
claim Hr8_range:
∀x : set, x ∈ A → apply_fun r8 x ∈ I2.
Let x be given.
We prove the intermediate
claim Hr7sIx:
apply_fun r7s x ∈ I.
We prove the intermediate
claim HB8_cases:
x ∈ B8 ∨ ¬ (x ∈ B8).
An
exact proof term for the current goal is
(xm (x ∈ B8)).
Apply (HB8_cases (apply_fun r8 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu8_on_B8 x HxB8).
rewrite the current goal using (Hr8_apply x HxA) (from left to right).
rewrite the current goal using Hu8eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr8eq (from left to right).
We prove the intermediate
claim Hr7sI1I:
apply_fun r7s x ∈ I1 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r7s x0 ∈ I1 ∩ I) x HxB8).
We prove the intermediate
claim Hr7sI1:
apply_fun r7s x ∈ I1.
We prove the intermediate
claim Hr7sRx:
apply_fun r7s x ∈ R.
An exact proof term for the current goal is Hlow_tmp.
An exact proof term for the current goal is Hup0_tmp.
We prove the intermediate
claim HC8_cases:
x ∈ C8 ∨ ¬ (x ∈ C8).
An
exact proof term for the current goal is
(xm (x ∈ C8)).
Apply (HC8_cases (apply_fun r8 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu8_on_C8 x HxC8).
rewrite the current goal using (Hr8_apply x HxA) (from left to right).
rewrite the current goal using Hu8eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr8eq (from left to right).
We prove the intermediate
claim Hr7sI3I:
apply_fun r7s x ∈ I3 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r7s x0 ∈ I3 ∩ I) x HxC8).
We prove the intermediate
claim Hr7sI3:
apply_fun r7s x ∈ I3.
We prove the intermediate
claim Hr7sRx:
apply_fun r7s x ∈ R.
An exact proof term for the current goal is H0le_tmp.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim HnotI1:
¬ (apply_fun r7s x ∈ I1).
We prove the intermediate
claim Hr7sI1I:
apply_fun r7s x ∈ I1 ∩ I.
We prove the intermediate
claim HxB8':
x ∈ B8.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r7s x0 ∈ I1 ∩ I) x HxA Hr7sI1I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotB8 HxB8').
We prove the intermediate
claim HnotI3:
¬ (apply_fun r7s x ∈ I3).
We prove the intermediate
claim Hr7sI3I:
apply_fun r7s x ∈ I3 ∩ I.
We prove the intermediate
claim HxC8':
x ∈ C8.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r7s x0 ∈ I3 ∩ I) x HxA Hr7sI3I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotC8 HxC8').
We prove the intermediate
claim Hr7sRx:
apply_fun r7s x ∈ R.
We prove the intermediate
claim Hnlt_1_fx:
¬ (Rlt 1 (apply_fun r7s x)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_fx_m1 Hbad).
An exact proof term for the current goal is Hok.
An exact proof term for the current goal is Hok.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1_fx Hbad).
We prove the intermediate
claim Hr7sI0:
apply_fun r7s x ∈ I0.
rewrite the current goal using HI0_def (from left to right).
An exact proof term for the current goal is HxSep.
We prove the intermediate
claim Hu8funI0:
function_on u8 X I0.
We prove the intermediate
claim Hu8xI0:
apply_fun u8 x ∈ I0.
An exact proof term for the current goal is (Hu8funI0 x HxX).
We prove the intermediate
claim Hu8xR:
apply_fun u8 x ∈ R.
rewrite the current goal using (Hr8_apply x HxA) (from left to right).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is Hlow_tmp.
rewrite the current goal using Hdef23 (from left to right) at position 1.
An exact proof term for the current goal is Hup_tmp.
We prove the intermediate
claim Hr8s_cont:
continuous_map A Ta I Ti r8s.
We prove the intermediate
claim Hr8s_I:
∀x : set, x ∈ A → apply_fun r8s x ∈ I.
Let x be given.
We prove the intermediate
claim Hr8xI2:
apply_fun r8 x ∈ I2.
An exact proof term for the current goal is (Hr8_range x HxA).
We prove the intermediate
claim HmdenR:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den H23R).
We prove the intermediate
claim Hr8xR:
apply_fun r8 x ∈ R.
We prove the intermediate
claim Hr8xS:
SNo (apply_fun r8 x).
We prove the intermediate
claim Hhi:
Rle (apply_fun r8 x) den.
We prove the intermediate
claim Hnlt_hi:
¬ (Rlt den (apply_fun r8 x)).
We prove the intermediate
claim HyR:
apply_fun r8s x ∈ R.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim Hy_le_1:
Rle (apply_fun r8s x) 1.
We prove the intermediate
claim H1lty:
1 < apply_fun r8s x.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
rewrite the current goal using HyEq (from left to right) at position 1.
We prove the intermediate
claim Hden_lt_r8x:
den < apply_fun r8 x.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate
claim Hbad:
Rlt den (apply_fun r8 x).
An
exact proof term for the current goal is
(RltI den (apply_fun r8 x) H23R Hr8xR Hden_lt_r8x).
An exact proof term for the current goal is (Hnlt_hi Hbad).
rewrite the current goal using HyEq (from left to right) at position 1.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
An
exact proof term for the current goal is
(RltI (apply_fun r8 x) (minus_SNo den) Hr8xR HmdenR Hr8x_lt_mden).
An exact proof term for the current goal is (Hnlt_lo Hbad).
Apply Hex_u9 to the current goal.
Let u9 be given.
Assume Hu9.
We prove the intermediate
claim Hu9contI0:
continuous_map X Tx I0 T0 u9.
We prove the intermediate
claim HI0subR:
I0 ⊆ R.
Set den9 to be the term
mul_SNo den8 den.
We prove the intermediate
claim Hden9R:
den9 ∈ R.
An
exact proof term for the current goal is
(real_mul_SNo den8 Hden8R den H23R).
We prove the intermediate
claim Hden9pos:
0 < den9.
We prove the intermediate
claim Hden8S:
SNo den8.
An
exact proof term for the current goal is
(real_SNo den8 Hden8R).
An
exact proof term for the current goal is
(mul_SNo_pos_pos den8 den Hden8S H23S Hden8pos HdenPos).
An
exact proof term for the current goal is
(add_two_continuous_R X Tx g8 u9s HTx Hg8cont Hu9s_cont).
An
exact proof term for the current goal is
(add_two_continuous_R A Ta r8s u9neg HTa Hr8s_contR Hu9neg_cont).
Let x be given.
rewrite the current goal using
(pair_map_apply A R R r8s u9neg x HxA) (from left to right).
We prove the intermediate
claim Hr8sxI:
apply_fun r8s x ∈ I.
We prove the intermediate
claim Hr8sxR:
apply_fun r8s x ∈ R.
An
exact proof term for the current goal is
(HIcR (apply_fun r8s x) Hr8sxI).
We prove the intermediate
claim Hu9negRx:
apply_fun u9neg x ∈ R.
rewrite the current goal using
(pair_map_apply A R R r8s u9neg x HxA) (from left to right).
We prove the intermediate
claim Hu9Rx:
apply_fun u9 x ∈ R.
Use reflexivity.
We prove the intermediate
claim Hr9_range:
∀x : set, x ∈ A → apply_fun r9 x ∈ I2.
Let x be given.
We prove the intermediate
claim Hr8sIx:
apply_fun r8s x ∈ I.
We prove the intermediate
claim HB9_cases:
x ∈ B9 ∨ ¬ (x ∈ B9).
An
exact proof term for the current goal is
(xm (x ∈ B9)).
Apply (HB9_cases (apply_fun r9 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu9_on_B9 x HxB9).
rewrite the current goal using (Hr9_apply x HxA) (from left to right).
rewrite the current goal using Hu9eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr9eq (from left to right).
We prove the intermediate
claim Hr8sI1I:
apply_fun r8s x ∈ I1 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r8s x0 ∈ I1 ∩ I) x HxB9).
We prove the intermediate
claim Hr8sI1:
apply_fun r8s x ∈ I1.
We prove the intermediate
claim Hr8sRx:
apply_fun r8s x ∈ R.
An exact proof term for the current goal is Hlow_tmp.
An exact proof term for the current goal is Hup0_tmp.
We prove the intermediate
claim HC9_cases:
x ∈ C9 ∨ ¬ (x ∈ C9).
An
exact proof term for the current goal is
(xm (x ∈ C9)).
Apply (HC9_cases (apply_fun r9 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu9_on_C9 x HxC9).
rewrite the current goal using (Hr9_apply x HxA) (from left to right).
rewrite the current goal using Hu9eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr9eq (from left to right).
We prove the intermediate
claim Hr8sI3I:
apply_fun r8s x ∈ I3 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r8s x0 ∈ I3 ∩ I) x HxC9).
We prove the intermediate
claim Hr8sI3:
apply_fun r8s x ∈ I3.
We prove the intermediate
claim Hr8sRx:
apply_fun r8s x ∈ R.
An exact proof term for the current goal is H0le_tmp.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim HnotI1:
¬ (apply_fun r8s x ∈ I1).
We prove the intermediate
claim Hr8sI1I:
apply_fun r8s x ∈ I1 ∩ I.
We prove the intermediate
claim HxB9':
x ∈ B9.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r8s x0 ∈ I1 ∩ I) x HxA Hr8sI1I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotB9 HxB9').
We prove the intermediate
claim HnotI3:
¬ (apply_fun r8s x ∈ I3).
We prove the intermediate
claim Hr8sI3I:
apply_fun r8s x ∈ I3 ∩ I.
We prove the intermediate
claim HxC9':
x ∈ C9.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r8s x0 ∈ I3 ∩ I) x HxA Hr8sI3I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotC9 HxC9').
We prove the intermediate
claim Hr8sRx:
apply_fun r8s x ∈ R.
We prove the intermediate
claim Hnlt_1_fx:
¬ (Rlt 1 (apply_fun r8s x)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_fx_m1 Hbad).
An exact proof term for the current goal is Hok.
An exact proof term for the current goal is Hok.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1_fx Hbad).
We prove the intermediate
claim Hr8sI0:
apply_fun r8s x ∈ I0.
rewrite the current goal using HI0_def (from left to right).
An exact proof term for the current goal is HxSep.
We prove the intermediate
claim Hu9funI0:
function_on u9 X I0.
We prove the intermediate
claim Hu9xI0:
apply_fun u9 x ∈ I0.
An exact proof term for the current goal is (Hu9funI0 x HxX).
We prove the intermediate
claim Hu9xR:
apply_fun u9 x ∈ R.
rewrite the current goal using (Hr9_apply x HxA) (from left to right).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is Hlow_tmp.
rewrite the current goal using Hdef23 (from left to right) at position 1.
An exact proof term for the current goal is Hup_tmp.
We prove the intermediate
claim Hr9s_cont:
continuous_map A Ta I Ti r9s.
We prove the intermediate
claim Hr9s_I:
∀x : set, x ∈ A → apply_fun r9s x ∈ I.
Let x be given.
We prove the intermediate
claim Hr9xI2:
apply_fun r9 x ∈ I2.
An exact proof term for the current goal is (Hr9_range x HxA).
We prove the intermediate
claim HmdenR:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den H23R).
We prove the intermediate
claim Hr9xR:
apply_fun r9 x ∈ R.
We prove the intermediate
claim Hr9xS:
SNo (apply_fun r9 x).
We prove the intermediate
claim Hhi:
Rle (apply_fun r9 x) den.
We prove the intermediate
claim Hnlt_hi:
¬ (Rlt den (apply_fun r9 x)).
We prove the intermediate
claim HyR:
apply_fun r9s x ∈ R.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim Hy_le_1:
Rle (apply_fun r9s x) 1.
We prove the intermediate
claim H1lty:
1 < apply_fun r9s x.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
rewrite the current goal using HyEq (from left to right) at position 1.
We prove the intermediate
claim Hden_lt_r9x:
den < apply_fun r9 x.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate
claim Hbad:
Rlt den (apply_fun r9 x).
An
exact proof term for the current goal is
(RltI den (apply_fun r9 x) H23R Hr9xR Hden_lt_r9x).
An exact proof term for the current goal is (Hnlt_hi Hbad).
rewrite the current goal using HyEq (from left to right) at position 1.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
An
exact proof term for the current goal is
(RltI (apply_fun r9 x) (minus_SNo den) Hr9xR HmdenR Hr9x_lt_mden).
An exact proof term for the current goal is (Hnlt_lo Hbad).
Apply Hex_u10 to the current goal.
Let u10 be given.
Assume Hu10.
We prove the intermediate
claim Hu10contI0:
continuous_map X Tx I0 T0 u10.
We prove the intermediate
claim HI0subR:
I0 ⊆ R.
Set den10 to be the term
mul_SNo den9 den.
We prove the intermediate
claim Hden10R:
den10 ∈ R.
An
exact proof term for the current goal is
(real_mul_SNo den9 Hden9R den H23R).
We prove the intermediate
claim Hden10pos:
0 < den10.
We prove the intermediate
claim Hden9S:
SNo den9.
An
exact proof term for the current goal is
(real_SNo den9 Hden9R).
An
exact proof term for the current goal is
(mul_SNo_pos_pos den9 den Hden9S H23S Hden9pos HdenPos).
An
exact proof term for the current goal is
(add_two_continuous_R X Tx g9 u10s HTx Hg9cont Hu10s_cont).
An exact proof term for the current goal is HTiEq.
An
exact proof term for the current goal is
(add_two_continuous_R A Ta r9s u10neg HTa Hr9s_contR Hu10neg_cont).
Let x be given.
rewrite the current goal using
(pair_map_apply A R R r9s u10neg x HxA) (from left to right).
We prove the intermediate
claim Hr9sxI:
apply_fun r9s x ∈ I.
We prove the intermediate
claim Hr9sxR:
apply_fun r9s x ∈ R.
An
exact proof term for the current goal is
(HIcR (apply_fun r9s x) Hr9sxI).
We prove the intermediate
claim Hu10negRx:
apply_fun u10neg x ∈ R.
rewrite the current goal using
(pair_map_apply A R R r9s u10neg x HxA) (from left to right).
We prove the intermediate
claim Hu10Rx:
apply_fun u10 x ∈ R.
Use reflexivity.
We prove the intermediate
claim Hr10_range:
∀x : set, x ∈ A → apply_fun r10 x ∈ I2.
Let x be given.
We prove the intermediate
claim Hr9sIx:
apply_fun r9s x ∈ I.
We prove the intermediate
claim HB10_cases:
x ∈ B10 ∨ ¬ (x ∈ B10).
An
exact proof term for the current goal is
(xm (x ∈ B10)).
Apply (HB10_cases (apply_fun r10 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu10_on_B10 x HxB10).
rewrite the current goal using (Hr10_apply x HxA) (from left to right).
rewrite the current goal using Hu10eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr10eq (from left to right).
We prove the intermediate
claim Hr9sI1I:
apply_fun r9s x ∈ I1 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r9s x0 ∈ I1 ∩ I) x HxB10).
We prove the intermediate
claim Hr9sI1:
apply_fun r9s x ∈ I1.
We prove the intermediate
claim Hr9sRx:
apply_fun r9s x ∈ R.
An exact proof term for the current goal is Hlow_tmp.
An exact proof term for the current goal is Hup0_tmp.
We prove the intermediate
claim HC10_cases:
x ∈ C10 ∨ ¬ (x ∈ C10).
An
exact proof term for the current goal is
(xm (x ∈ C10)).
Apply (HC10_cases (apply_fun r10 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu10_on_C10 x HxC10).
rewrite the current goal using (Hr10_apply x HxA) (from left to right).
rewrite the current goal using Hu10eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr10eq (from left to right).
We prove the intermediate
claim Hr9sI3I:
apply_fun r9s x ∈ I3 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r9s x0 ∈ I3 ∩ I) x HxC10).
We prove the intermediate
claim Hr9sI3:
apply_fun r9s x ∈ I3.
We prove the intermediate
claim Hr9sRx:
apply_fun r9s x ∈ R.
An exact proof term for the current goal is H0le_tmp.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim HnotI1:
¬ (apply_fun r9s x ∈ I1).
We prove the intermediate
claim Hr9sI1I:
apply_fun r9s x ∈ I1 ∩ I.
We prove the intermediate
claim HxB10':
x ∈ B10.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r9s x0 ∈ I1 ∩ I) x HxA Hr9sI1I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotB10 HxB10').
We prove the intermediate
claim HnotI3:
¬ (apply_fun r9s x ∈ I3).
We prove the intermediate
claim Hr9sI3I:
apply_fun r9s x ∈ I3 ∩ I.
We prove the intermediate
claim HxC10':
x ∈ C10.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r9s x0 ∈ I3 ∩ I) x HxA Hr9sI3I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotC10 HxC10').
We prove the intermediate
claim Hr9sRx:
apply_fun r9s x ∈ R.
We prove the intermediate
claim Hnlt_1_fx:
¬ (Rlt 1 (apply_fun r9s x)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_fx_m1 Hbad).
An exact proof term for the current goal is Hok.
An exact proof term for the current goal is Hok.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1_fx Hbad).
We prove the intermediate
claim Hr9sI0:
apply_fun r9s x ∈ I0.
rewrite the current goal using HI0_def (from left to right).
An exact proof term for the current goal is HxSep.
We prove the intermediate
claim Hu10funI0:
function_on u10 X I0.
We prove the intermediate
claim Hu10xI0:
apply_fun u10 x ∈ I0.
An exact proof term for the current goal is (Hu10funI0 x HxX).
We prove the intermediate
claim Hu10xR:
apply_fun u10 x ∈ R.
rewrite the current goal using (Hr10_apply x HxA) (from left to right).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is Hlow_tmp.
rewrite the current goal using Hdef23 (from left to right) at position 1.
An exact proof term for the current goal is Hup_tmp.
We prove the intermediate
claim Hr10s_cont:
continuous_map A Ta I Ti r10s.
We prove the intermediate
claim Hr10s_I:
∀x : set, x ∈ A → apply_fun r10s x ∈ I.
Let x be given.
We prove the intermediate
claim Hr10xI2:
apply_fun r10 x ∈ I2.
An exact proof term for the current goal is (Hr10_range x HxA).
We prove the intermediate
claim HmdenR:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den H23R).
We prove the intermediate
claim Hr10xR:
apply_fun r10 x ∈ R.
We prove the intermediate
claim Hr10xS:
SNo (apply_fun r10 x).
We prove the intermediate
claim Hhi:
Rle (apply_fun r10 x) den.
We prove the intermediate
claim Hnlt_hi:
¬ (Rlt den (apply_fun r10 x)).
We prove the intermediate
claim HyR:
apply_fun r10s x ∈ R.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim HyS:
SNo (apply_fun r10s x).
We prove the intermediate
claim Hy_le_1:
Rle (apply_fun r10s x) 1.
We prove the intermediate
claim H1lty:
1 < apply_fun r10s x.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
rewrite the current goal using HyEq (from left to right) at position 1.
We prove the intermediate
claim Hden_lt_r10x:
den < apply_fun r10 x.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate
claim Hbad:
Rlt den (apply_fun r10 x).
An
exact proof term for the current goal is
(RltI den (apply_fun r10 x) H23R Hr10xR Hden_lt_r10x).
An exact proof term for the current goal is (Hnlt_hi Hbad).
rewrite the current goal using HyEq (from left to right) at position 1.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
An
exact proof term for the current goal is
(RltI (apply_fun r10 x) (minus_SNo den) Hr10xR HmdenR Hr10x_lt_mden).
An exact proof term for the current goal is (Hnlt_lo Hbad).
Apply Hex_u11 to the current goal.
Let u11 be given.
Assume Hu11.
We prove the intermediate
claim Hu11contI0:
continuous_map X Tx I0 T0 u11.
We prove the intermediate
claim HI0subR:
I0 ⊆ R.
Set den11 to be the term
mul_SNo den10 den.
We prove the intermediate
claim Hden11R:
den11 ∈ R.
An
exact proof term for the current goal is
(real_mul_SNo den10 Hden10R den H23R).
We prove the intermediate
claim Hden11pos:
0 < den11.
We prove the intermediate
claim Hden10S:
SNo den10.
An
exact proof term for the current goal is
(real_SNo den10 Hden10R).
An
exact proof term for the current goal is
(mul_SNo_pos_pos den10 den Hden10S H23S Hden10pos HdenPos).
An
exact proof term for the current goal is
(add_two_continuous_R X Tx g10 u11s HTx Hg10cont Hu11s_cont).
An exact proof term for the current goal is HTiEq.
An
exact proof term for the current goal is
(add_two_continuous_R A Ta r10s u11neg HTa Hr10s_contR Hu11neg_cont).
Let x be given.
rewrite the current goal using
(pair_map_apply A R R r10s u11neg x HxA) (from left to right).
We prove the intermediate
claim Hr10sxI:
apply_fun r10s x ∈ I.
We prove the intermediate
claim Hr10sxR:
apply_fun r10s x ∈ R.
An
exact proof term for the current goal is
(HIcR (apply_fun r10s x) Hr10sxI).
We prove the intermediate
claim Hu11negRx:
apply_fun u11neg x ∈ R.
rewrite the current goal using
(pair_map_apply A R R r10s u11neg x HxA) (from left to right).
We prove the intermediate
claim Hu11Rx:
apply_fun u11 x ∈ R.
Use reflexivity.
We prove the intermediate
claim Hr11_range:
∀x : set, x ∈ A → apply_fun r11 x ∈ I2.
Let x be given.
We prove the intermediate
claim Hr10sIx:
apply_fun r10s x ∈ I.
We prove the intermediate
claim HB11_cases:
x ∈ B11 ∨ ¬ (x ∈ B11).
An
exact proof term for the current goal is
(xm (x ∈ B11)).
Apply (HB11_cases (apply_fun r11 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu11_on_B11 x HxB11).
rewrite the current goal using (Hr11_apply x HxA) (from left to right).
rewrite the current goal using Hu11eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr11eq (from left to right).
We prove the intermediate
claim Hr10sI1I:
apply_fun r10s x ∈ I1 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r10s x0 ∈ I1 ∩ I) x HxB11).
We prove the intermediate
claim Hr10sI1:
apply_fun r10s x ∈ I1.
We prove the intermediate
claim Hr10sRx:
apply_fun r10s x ∈ R.
An exact proof term for the current goal is Hlow_tmp.
An exact proof term for the current goal is Hup0_tmp.
We prove the intermediate
claim HC11_cases:
x ∈ C11 ∨ ¬ (x ∈ C11).
An
exact proof term for the current goal is
(xm (x ∈ C11)).
Apply (HC11_cases (apply_fun r11 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu11_on_C11 x HxC11).
rewrite the current goal using (Hr11_apply x HxA) (from left to right).
rewrite the current goal using Hu11eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr11eq (from left to right).
We prove the intermediate
claim Hr10sI3I:
apply_fun r10s x ∈ I3 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r10s x0 ∈ I3 ∩ I) x HxC11).
We prove the intermediate
claim Hr10sI3:
apply_fun r10s x ∈ I3.
We prove the intermediate
claim Hr10sRx:
apply_fun r10s x ∈ R.
An exact proof term for the current goal is H0le_tmp.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim HnotI1:
¬ (apply_fun r10s x ∈ I1).
We prove the intermediate
claim Hr10sI1I:
apply_fun r10s x ∈ I1 ∩ I.
We prove the intermediate
claim HxB11':
x ∈ B11.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r10s x0 ∈ I1 ∩ I) x HxA Hr10sI1I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotB11 HxB11').
We prove the intermediate
claim HnotI3:
¬ (apply_fun r10s x ∈ I3).
We prove the intermediate
claim Hr10sI3I:
apply_fun r10s x ∈ I3 ∩ I.
We prove the intermediate
claim HxC11':
x ∈ C11.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r10s x0 ∈ I3 ∩ I) x HxA Hr10sI3I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotC11 HxC11').
We prove the intermediate
claim Hr10sRx:
apply_fun r10s x ∈ R.
We prove the intermediate
claim Hnlt_1_fx:
¬ (Rlt 1 (apply_fun r10s x)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_fx_m1 Hbad).
An exact proof term for the current goal is Hok.
An exact proof term for the current goal is Hok.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1_fx Hbad).
We prove the intermediate
claim Hr10sI0:
apply_fun r10s x ∈ I0.
rewrite the current goal using HI0_def (from left to right).
An exact proof term for the current goal is HxSep.
We prove the intermediate
claim Hu11funI0:
function_on u11 X I0.
We prove the intermediate
claim Hu11xI0:
apply_fun u11 x ∈ I0.
An exact proof term for the current goal is (Hu11funI0 x HxX).
We prove the intermediate
claim Hu11xR:
apply_fun u11 x ∈ R.
rewrite the current goal using (Hr11_apply x HxA) (from left to right).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is Hlow_tmp.
rewrite the current goal using Hdef23 (from left to right) at position 1.
An exact proof term for the current goal is Hup_tmp.
We prove the intermediate
claim Hr11s_cont:
continuous_map A Ta I Ti r11s.
We prove the intermediate
claim Hr11s_I:
∀x : set, x ∈ A → apply_fun r11s x ∈ I.
Let x be given.
We prove the intermediate
claim Hr11xI2:
apply_fun r11 x ∈ I2.
An exact proof term for the current goal is (Hr11_range x HxA).
We prove the intermediate
claim HmdenR:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den H23R).
We prove the intermediate
claim Hr11xR:
apply_fun r11 x ∈ R.
We prove the intermediate
claim Hr11xS:
SNo (apply_fun r11 x).
We prove the intermediate
claim Hhi:
Rle (apply_fun r11 x) den.
We prove the intermediate
claim Hnlt_hi:
¬ (Rlt den (apply_fun r11 x)).
We prove the intermediate
claim HyR:
apply_fun r11s x ∈ R.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim HyS:
SNo (apply_fun r11s x).
We prove the intermediate
claim Hy_le_1:
Rle (apply_fun r11s x) 1.
We prove the intermediate
claim H1lty:
1 < apply_fun r11s x.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
rewrite the current goal using HyEq (from left to right) at position 1.
We prove the intermediate
claim Hden_lt_r11x:
den < apply_fun r11 x.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate
claim Hbad:
Rlt den (apply_fun r11 x).
An
exact proof term for the current goal is
(RltI den (apply_fun r11 x) H23R Hr11xR Hden_lt_r11x).
An exact proof term for the current goal is (Hnlt_hi Hbad).
rewrite the current goal using HyEq (from left to right) at position 1.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
An
exact proof term for the current goal is
(RltI (apply_fun r11 x) (minus_SNo den) Hr11xR HmdenR Hr11x_lt_mden).
An exact proof term for the current goal is (Hnlt_lo Hbad).
Apply Hex_u12 to the current goal.
Let u12 be given.
Assume Hu12.
We prove the intermediate
claim Hu12contI0:
continuous_map X Tx I0 T0 u12.
We prove the intermediate
claim HI0subR:
I0 ⊆ R.
Set den12 to be the term
mul_SNo den11 den.
We prove the intermediate
claim Hden12R:
den12 ∈ R.
An
exact proof term for the current goal is
(real_mul_SNo den11 Hden11R den H23R).
We prove the intermediate
claim Hden12pos:
0 < den12.
We prove the intermediate
claim Hden11S:
SNo den11.
An
exact proof term for the current goal is
(real_SNo den11 Hden11R).
An
exact proof term for the current goal is
(mul_SNo_pos_pos den11 den Hden11S H23S Hden11pos HdenPos).
An
exact proof term for the current goal is
(add_two_continuous_R X Tx g11 u12s HTx Hg11cont Hu12s_cont).
An exact proof term for the current goal is HTiEq.
An
exact proof term for the current goal is
(add_two_continuous_R A Ta r11s u12neg HTa Hr11s_contR Hu12neg_cont).
Let x be given.
rewrite the current goal using
(pair_map_apply A R R r11s u12neg x HxA) (from left to right).
We prove the intermediate
claim Hr11sxI:
apply_fun r11s x ∈ I.
We prove the intermediate
claim Hr11sxR:
apply_fun r11s x ∈ R.
An
exact proof term for the current goal is
(HIcR (apply_fun r11s x) Hr11sxI).
We prove the intermediate
claim Hu12negRx:
apply_fun u12neg x ∈ R.
rewrite the current goal using
(pair_map_apply A R R r11s u12neg x HxA) (from left to right).
We prove the intermediate
claim Hu12Rx:
apply_fun u12 x ∈ R.
Use reflexivity.
We prove the intermediate
claim Hr12_range:
∀x : set, x ∈ A → apply_fun r12 x ∈ I2.
Let x be given.
We prove the intermediate
claim Hr11sIx:
apply_fun r11s x ∈ I.
We prove the intermediate
claim HB12_cases:
x ∈ B12 ∨ ¬ (x ∈ B12).
An
exact proof term for the current goal is
(xm (x ∈ B12)).
Apply (HB12_cases (apply_fun r12 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu12_on_B12 x HxB12).
rewrite the current goal using (Hr12_apply x HxA) (from left to right).
rewrite the current goal using Hu12eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr12eq (from left to right).
We prove the intermediate
claim Hr11sI1I:
apply_fun r11s x ∈ I1 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r11s x0 ∈ I1 ∩ I) x HxB12).
We prove the intermediate
claim Hr11sI1:
apply_fun r11s x ∈ I1.
We prove the intermediate
claim Hr11sRx:
apply_fun r11s x ∈ R.
An exact proof term for the current goal is Hlow_tmp.
An exact proof term for the current goal is Hup0_tmp.
We prove the intermediate
claim HC12_cases:
x ∈ C12 ∨ ¬ (x ∈ C12).
An
exact proof term for the current goal is
(xm (x ∈ C12)).
Apply (HC12_cases (apply_fun r12 x ∈ I2)) to the current goal.
An exact proof term for the current goal is (Hu12_on_C12 x HxC12).
rewrite the current goal using (Hr12_apply x HxA) (from left to right).
rewrite the current goal using Hu12eq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr12eq (from left to right).
We prove the intermediate
claim Hr11sI3I:
apply_fun r11s x ∈ I3 ∩ I.
An
exact proof term for the current goal is
(SepE2 A (λx0 : set ⇒ apply_fun r11s x0 ∈ I3 ∩ I) x HxC12).
We prove the intermediate
claim Hr11sI3:
apply_fun r11s x ∈ I3.
We prove the intermediate
claim Hr11sRx:
apply_fun r11s x ∈ R.
An exact proof term for the current goal is H0le_tmp.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim HnotI1:
¬ (apply_fun r11s x ∈ I1).
We prove the intermediate
claim Hr11sI1I:
apply_fun r11s x ∈ I1 ∩ I.
We prove the intermediate
claim HxB12':
x ∈ B12.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r11s x0 ∈ I1 ∩ I) x HxA Hr11sI1I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotB12 HxB12').
We prove the intermediate
claim HnotI3:
¬ (apply_fun r11s x ∈ I3).
We prove the intermediate
claim Hr11sI3I:
apply_fun r11s x ∈ I3 ∩ I.
We prove the intermediate
claim HxC12':
x ∈ C12.
An
exact proof term for the current goal is
(SepI A (λx0 : set ⇒ apply_fun r11s x0 ∈ I3 ∩ I) x HxA Hr11sI3I).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxnotC12 HxC12').
We prove the intermediate
claim Hr11sRx:
apply_fun r11s x ∈ R.
We prove the intermediate
claim Hnlt_1_fx:
¬ (Rlt 1 (apply_fun r11s x)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_fx_m1 Hbad).
An exact proof term for the current goal is Hok.
An exact proof term for the current goal is Hok.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt_1_fx Hbad).
We prove the intermediate
claim Hr11sI0:
apply_fun r11s x ∈ I0.
rewrite the current goal using HI0_def (from left to right).
An exact proof term for the current goal is HxSep.
We prove the intermediate
claim Hu12funI0:
function_on u12 X I0.
We prove the intermediate
claim Hu12xI0:
apply_fun u12 x ∈ I0.
An exact proof term for the current goal is (Hu12funI0 x HxX).
We prove the intermediate
claim Hu12xR:
apply_fun u12 x ∈ R.
rewrite the current goal using (Hr12_apply x HxA) (from left to right).
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is Hlow_tmp.
rewrite the current goal using Hdef23 (from left to right) at position 1.
An exact proof term for the current goal is Hup_tmp.
We prove the intermediate
claim Hr12s_cont:
continuous_map A Ta I Ti r12s.
We prove the intermediate
claim Hr12s_I:
∀x : set, x ∈ A → apply_fun r12s x ∈ I.
Let x be given.
We prove the intermediate
claim Hr12xI2:
apply_fun r12 x ∈ I2.
An exact proof term for the current goal is (Hr12_range x HxA).
We prove the intermediate
claim HmdenR:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den H23R).
We prove the intermediate
claim Hr12xR:
apply_fun r12 x ∈ R.
We prove the intermediate
claim Hr12xS:
SNo (apply_fun r12 x).
We prove the intermediate
claim Hhi:
Rle (apply_fun r12 x) den.
We prove the intermediate
claim Hnlt_hi:
¬ (Rlt den (apply_fun r12 x)).
We prove the intermediate
claim HyR:
apply_fun r12s x ∈ R.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim HyS:
SNo (apply_fun r12s x).
We prove the intermediate
claim Hy_le_1:
Rle (apply_fun r12s x) 1.
We prove the intermediate
claim H1lty:
1 < apply_fun r12s x.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
rewrite the current goal using HyEq (from left to right) at position 1.
We prove the intermediate
claim Hden_lt_r12x:
den < apply_fun r12 x.
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt'.
We prove the intermediate
claim Hbad:
Rlt den (apply_fun r12 x).
An
exact proof term for the current goal is
(RltI den (apply_fun r12 x) H23R Hr12xR Hden_lt_r12x).
An exact proof term for the current goal is (Hnlt_hi Hbad).
rewrite the current goal using HyEq (from left to right) at position 1.
rewrite the current goal using
(mul_SNo_oneL den H23S) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HmulEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is HmulLt.
An
exact proof term for the current goal is
(RltI (apply_fun r12 x) (minus_SNo den) Hr12xR HmdenR Hr12x_lt_mden).
An exact proof term for the current goal is (Hnlt_lo Hbad).
Let r be given.
We prove the intermediate
claim Hexu:
∃u : set, P u.
Apply Hexu to the current goal.
Let u be given.
Assume Hu.
We prove the intermediate
claim HP:
P (Eps_i P).
An
exact proof term for the current goal is
(Eps_i_ax P u Hu).
We prove the intermediate
claim Hu_eq:
u_of r = Eps_i P.
rewrite the current goal using Hu_eq (from left to right).
An exact proof term for the current goal is HP.
Set BaseState to be the term (g0g,(f1s,den)).
Set State to be the term
(λn : set ⇒ nat_primrec BaseState StepState n).
Set fn to be the term
graph ω (λn : set ⇒ (State n) 0).
We use fn to witness the existential quantifier.
We prove the intermediate
claim HInv_cpos:
∀n : set, n ∈ ω → ((State n) 1) 1 ∈ R ∧ 0 < ((State n) 1) 1.
We prove the intermediate
claim HInv_nat:
∀n : set, nat_p n → ((State n) 1) 1 ∈ R ∧ 0 < ((State n) 1) 1.
We will
prove ((State 0) 1) 1 ∈ R ∧ 0 < ((State 0) 1) 1.
We prove the intermediate
claim H0:
State 0 = BaseState.
An
exact proof term for the current goal is
(nat_primrec_0 BaseState StepState).
rewrite the current goal using H0 (from left to right).
We prove the intermediate
claim HBase:
BaseState = (g0g,(f1s,den)).
rewrite the current goal using HBase (from left to right).
We prove the intermediate
claim HtEq:
((g0g,(f1s,den)) 1) 1 = den.
rewrite the current goal using
(tuple_2_1_eq g0g (f1s,den)) (from left to right) at position 1.
rewrite the current goal using
(tuple_2_1_eq f1s den) (from left to right) at position 1.
Use reflexivity.
Apply andI to the current goal.
rewrite the current goal using HtEq (from left to right).
An exact proof term for the current goal is HdenR.
rewrite the current goal using HtEq (from left to right).
An exact proof term for the current goal is HdenPos.
Let n be given.
We prove the intermediate
claim HS:
State (ordsucc n) = StepState n (State n).
An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState n HnNat).
rewrite the current goal using HS (from left to right).
Set st to be the term State n.
Set g to be the term
st 0.
Set rpack to be the term
st 1.
Set r to be the term
rpack 0.
Set c to be the term
rpack 1.
Set cNew to be the term
mul_SNo c den.
We prove the intermediate
claim Hdef:
StepState n st = (gNew,(rNew,cNew)).
We prove the intermediate
claim HtEq:
((StepState n st) 1) 1 = cNew.
We prove the intermediate
claim Hinner:
(StepState n st) 1 = (rNew,cNew).
rewrite the current goal using Hdef (from left to right).
An
exact proof term for the current goal is
(tuple_2_1_eq gNew (rNew,cNew)).
rewrite the current goal using Hinner (from left to right).
An
exact proof term for the current goal is
(tuple_2_1_eq rNew cNew).
We prove the intermediate
claim Hc_eq:
c = ((State n) 1) 1.
We prove the intermediate
claim HcR0:
((State n) 1) 1 ∈ R.
An
exact proof term for the current goal is
(andEL (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) IH).
We prove the intermediate
claim Hcpos0:
0 < ((State n) 1) 1.
An
exact proof term for the current goal is
(andER (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) IH).
We prove the intermediate
claim HcR:
c ∈ R.
rewrite the current goal using Hc_eq (from left to right).
An exact proof term for the current goal is HcR0.
We prove the intermediate
claim Hcpos:
0 < c.
rewrite the current goal using Hc_eq (from left to right).
An exact proof term for the current goal is Hcpos0.
We prove the intermediate
claim HcS:
SNo c.
An
exact proof term for the current goal is
(real_SNo c HcR).
We prove the intermediate
claim HdenS:
SNo den.
An
exact proof term for the current goal is
(real_SNo den HdenR).
We prove the intermediate
claim HcNewR:
cNew ∈ R.
An
exact proof term for the current goal is
(real_mul_SNo c HcR den HdenR).
We prove the intermediate
claim HcNewPos:
0 < cNew.
An
exact proof term for the current goal is
(mul_SNo_pos_pos c den HcS HdenS Hcpos HdenPos).
Apply andI to the current goal.
rewrite the current goal using HtEq (from left to right).
An exact proof term for the current goal is HcNewR.
rewrite the current goal using HtEq (from left to right).
An exact proof term for the current goal is HcNewPos.
Let n be given.
An
exact proof term for the current goal is
(HInv_nat n (omega_nat_p n HnO)).
We prove the intermediate
claim HInv_c_lt1:
∀n : set, n ∈ ω → ((State n) 1) 1 < 1.
We prove the intermediate
claim HInv_nat:
∀n : set, nat_p n → ((State n) 1) 1 < 1.
We will
prove ((State 0) 1) 1 < 1.
We prove the intermediate
claim H0:
State 0 = BaseState.
An
exact proof term for the current goal is
(nat_primrec_0 BaseState StepState).
rewrite the current goal using H0 (from left to right).
We prove the intermediate
claim HBase:
BaseState = (g0g,(f1s,den)).
rewrite the current goal using HBase (from left to right).
We prove the intermediate
claim HtEq:
((g0g,(f1s,den)) 1) 1 = den.
rewrite the current goal using
(tuple_2_1_eq g0g (f1s,den)) (from left to right) at position 1.
rewrite the current goal using
(tuple_2_1_eq f1s den) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HtEq (from left to right).
We prove the intermediate
claim HdenDef:
den = two_thirds.
rewrite the current goal using HdenDef (from left to right).
Let n be given.
We prove the intermediate
claim HS:
State (ordsucc n) = StepState n (State n).
An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState n HnNat).
rewrite the current goal using HS (from left to right).
Set st to be the term State n.
Set g to be the term
st 0.
Set rpack to be the term
st 1.
Set r to be the term
rpack 0.
Set c to be the term
rpack 1.
Set cNew to be the term
mul_SNo c den.
We prove the intermediate
claim Hdef:
StepState n st = (gNew,(rNew,cNew)).
We prove the intermediate
claim HtEq:
((StepState n st) 1) 1 = cNew.
We prove the intermediate
claim Hinner:
(StepState n st) 1 = (rNew,cNew).
rewrite the current goal using Hdef (from left to right).
An
exact proof term for the current goal is
(tuple_2_1_eq gNew (rNew,cNew)).
rewrite the current goal using Hinner (from left to right).
An
exact proof term for the current goal is
(tuple_2_1_eq rNew cNew).
rewrite the current goal using HtEq (from left to right).
We prove the intermediate
claim HnO:
n ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega n HnNat).
We prove the intermediate
claim Hcpack:
((State n) 1) 1 ∈ R ∧ 0 < ((State n) 1) 1.
An exact proof term for the current goal is (HInv_cpos n HnO).
We prove the intermediate
claim HcR:
((State n) 1) 1 ∈ R.
An
exact proof term for the current goal is
(andEL (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) Hcpack).
We prove the intermediate
claim Hcpos:
0 < ((State n) 1) 1.
An
exact proof term for the current goal is
(andER (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) Hcpack).
We prove the intermediate
claim HcS:
SNo (((State n) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State n) 1) 1) HcR).
We prove the intermediate
claim HdenDef:
den = two_thirds.
We prove the intermediate
claim HdenLt1:
den < 1.
rewrite the current goal using HdenDef (from left to right).
We prove the intermediate
claim HdenS:
SNo den.
An
exact proof term for the current goal is
(real_SNo den HdenR).
We prove the intermediate
claim HmulLt:
mul_SNo den (((State n) 1) 1) < ((State n) 1) 1.
An
exact proof term for the current goal is
(mul_SNo_Lt1_pos_Lt den (((State n) 1) 1) HdenS HcS HdenLt1 Hcpos).
We prove the intermediate
claim HmulEq:
mul_SNo den (((State n) 1) 1) = mul_SNo (((State n) 1) 1) den.
An
exact proof term for the current goal is
(mul_SNo_com den (((State n) 1) 1) HdenS HcS).
We prove the intermediate
claim HcNewLt:
cNew < ((State n) 1) 1.
We prove the intermediate
claim HcEq:
c = ((State n) 1) 1.
rewrite the current goal using HcEq (from left to right) at position 1.
rewrite the current goal using HmulEq (from right to left) at position 1.
An exact proof term for the current goal is HmulLt.
We prove the intermediate
claim HcNewR:
cNew ∈ R.
We prove the intermediate
claim HcEq:
c = ((State n) 1) 1.
rewrite the current goal using HcEq (from left to right).
An
exact proof term for the current goal is
(real_mul_SNo (((State n) 1) 1) HcR den HdenR).
We prove the intermediate
claim HcNewS:
SNo cNew.
An
exact proof term for the current goal is
(real_SNo cNew HcNewR).
An
exact proof term for the current goal is
(SNoLt_tra cNew (((State n) 1) 1) 1 HcNewS HcS SNo_1 HcNewLt IH).
Let n be given.
An
exact proof term for the current goal is
(HInv_nat n (omega_nat_p n HnO)).
We prove the intermediate
claim HInv_r_contI:
∀n : set, n ∈ ω → continuous_map A Ta I Ti (((State n) 1) 0).
We prove the intermediate
claim HInv_nat:
∀n : set, nat_p n → continuous_map A Ta I Ti (((State n) 1) 0).
We prove the intermediate
claim H0:
State 0 = BaseState.
An
exact proof term for the current goal is
(nat_primrec_0 BaseState StepState).
rewrite the current goal using H0 (from left to right).
We prove the intermediate
claim HBase:
BaseState = (g0g,(f1s,den)).
rewrite the current goal using HBase (from left to right).
We prove the intermediate
claim Hr0eq:
(((g0g,(f1s,den)) 1) 0) = f1s.
rewrite the current goal using
(tuple_2_1_eq g0g (f1s,den)) (from left to right) at position 1.
rewrite the current goal using
(tuple_2_0_eq f1s den) (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hr0eq (from left to right).
An exact proof term for the current goal is Hf1s_cont.
Let n be given.
We prove the intermediate
claim HS:
State (ordsucc n) = StepState n (State n).
An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState n HnNat).
rewrite the current goal using HS (from left to right).
Set st to be the term State n.
Set g to be the term
st 0.
Set rpack to be the term
st 1.
Set r to be the term
rpack 0.
Set c to be the term
rpack 1.
Set cNew to be the term
mul_SNo c den.
We prove the intermediate
claim Hdef:
StepState n st = (gNew,(rNew,cNew)).
We prove the intermediate
claim HrEq:
((StepState n st) 1) 0 = rNew.
We prove the intermediate
claim Hinner:
(StepState n st) 1 = (rNew,cNew).
rewrite the current goal using Hdef (from left to right).
An
exact proof term for the current goal is
(tuple_2_1_eq gNew (rNew,cNew)).
rewrite the current goal using Hinner (from left to right).
An
exact proof term for the current goal is
(tuple_2_0_eq rNew cNew).
rewrite the current goal using HrEq (from left to right).
We prove the intermediate
claim HIcR:
I ⊆ R.
We prove the intermediate
claim HrEq0:
r = ((State n) 1) 0.
rewrite the current goal using HrEq0 (from left to right).
An exact proof term for the current goal is IH.
An exact proof term for the current goal is (Hu_of_prop r Hr_contI).
We prove the intermediate
claim Hu_contI0:
continuous_map X Tx I0 T0 (u_of r).
We prove the intermediate
claim HI0cR:
I0 ⊆ R.
We prove the intermediate
claim HAsubX:
A ⊆ X.
We prove the intermediate
claim HrNew_img:
∀x : set, x ∈ A → apply_fun rNew x ∈ I.
Let x be given.
We prove the intermediate
claim HrNumI2:
apply_fun rNum x ∈ I2.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim Hfun_r:
function_on r A I.
We prove the intermediate
claim HrxI:
apply_fun r x ∈ I.
An exact proof term for the current goal is (Hfun_r x HxA).
We prove the intermediate
claim HrxR:
apply_fun r x ∈ R.
An
exact proof term for the current goal is
(HIcR (apply_fun r x) HrxI).
We prove the intermediate
claim Hfun_u:
function_on (u_of r) X I0.
We prove the intermediate
claim HuxI0:
apply_fun (u_of r) x ∈ I0.
An exact proof term for the current goal is (Hfun_u x HxX).
We prove the intermediate
claim HuxR:
apply_fun (u_of r) x ∈ R.
An
exact proof term for the current goal is
(HI0cR (apply_fun (u_of r) x) HuxI0).
An exact proof term for the current goal is (Hu_left_eq x HxPre).
rewrite the current goal using HrNumEq (from left to right).
rewrite the current goal using HuxEq (from left to right).
Use reflexivity.
rewrite the current goal using HrNumEqL (from left to right).
We prove the intermediate
claim HdenDef:
den = two_thirds.
We prove the intermediate
claim HmdenR:
(minus_SNo den) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den HdenR).
rewrite the current goal using HdenDef (from left to right) at position 1.
An exact proof term for the current goal is Hlow_tmp.
rewrite the current goal using HtEq0 (from left to right).
We prove the intermediate
claim H0leDen:
Rle 0 den.
rewrite the current goal using HdenDef (from left to right) at position 1.
An exact proof term for the current goal is (Hu_right_eq x HxPre).
rewrite the current goal using HrNumEq (from left to right).
rewrite the current goal using HuxEq (from left to right).
Use reflexivity.
rewrite the current goal using HrNumEqR (from left to right).
An exact proof term for the current goal is H0le_rNum_tmp.
We prove the intermediate
claim HdenDef:
den = two_thirds.
rewrite the current goal using HdenDef (from left to right) at position 1.
An exact proof term for the current goal is Hlow0.
rewrite the current goal using HdenDef (from left to right) at position 1.
An exact proof term for the current goal is Hup0.
We prove the intermediate
claim HmdenR:
minus_SNo den ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den HdenR).
An exact proof term for the current goal is Hr_not_lt_left.
An exact proof term for the current goal is Hr_not_lt_right.
rewrite the current goal using HrNumEq (from left to right).
An exact proof term for the current goal is Hm13R.
An exact proof term for the current goal is Hlow0.
We prove the intermediate
claim HdenDef:
den = two_thirds.
rewrite the current goal using HdenDef (from left to right) at position 1.
An exact proof term for the current goal is Hlow2.
rewrite the current goal using Htwo_def (from right to left) at position 1.
rewrite the current goal using HdenDef (from left to right) at position 1.
An exact proof term for the current goal is Hup2.
We prove the intermediate
claim HmdenR:
minus_SNo den ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo den HdenR).
We prove the intermediate
claim HrNumR:
apply_fun rNum x ∈ R.
rewrite the current goal using HrNewEq (from left to right).
rewrite the current goal using HTiEq (from left to right).
An exact proof term for the current goal is HrNew_contI'.
Let n be given.
An
exact proof term for the current goal is
(HInv_nat n (omega_nat_p n HnO)).
We prove the intermediate
claim HInv_g_R_A:
∀n : set, n ∈ ω → ∀x : set, x ∈ A → apply_fun ((State n) 0) x ∈ R.
We prove the intermediate
claim HInv_nat:
∀n : set, nat_p n → ∀x : set, x ∈ A → apply_fun ((State n) 0) x ∈ R.
Let x be given.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim H0:
State 0 = BaseState.
An
exact proof term for the current goal is
(nat_primrec_0 BaseState StepState).
rewrite the current goal using H0 (from left to right).
We prove the intermediate
claim HBase:
BaseState = (g0g,(f1s,den)).
rewrite the current goal using HBase (from left to right).
rewrite the current goal using
(tuple_2_0_eq g0g (f1s,den)) (from left to right).
We prove the intermediate
claim Hg0I0:
apply_fun g0 x ∈ I0.
An exact proof term for the current goal is (Hfung0 x HxX).
Let k be given.
Let x be given.
We prove the intermediate
claim HS:
State (ordsucc k) = StepState k (State k).
An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState k HkNat).
rewrite the current goal using HS (from left to right).
We prove the intermediate
claim HkO:
k ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega k HkNat).
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
Set st to be the term State k.
Set g to be the term
st 0.
Set rpack to be the term
st 1.
Set r to be the term
rpack 0.
Set c to be the term
rpack 1.
Set cNew to be the term
mul_SNo c den.
We prove the intermediate
claim Hdef:
StepState k st = (gNew,(rNew,cNew)).
We prove the intermediate
claim HgStep:
(StepState k st) 0 = gNew.
rewrite the current goal using Hdef (from left to right).
An
exact proof term for the current goal is
(tuple_2_0_eq gNew (rNew,cNew)).
rewrite the current goal using HgStep (from left to right).
We prove the intermediate
claim HgEq:
g = (State k) 0.
We prove the intermediate
claim HgxR:
apply_fun g x ∈ R.
rewrite the current goal using HgEq (from left to right).
An exact proof term for the current goal is (IH x HxA).
We prove the intermediate
claim HrEq:
r = ((State k) 1) 0.
rewrite the current goal using HrEq (from left to right).
An exact proof term for the current goal is (HInv_r_contI k HkO).
An exact proof term for the current goal is (Hu_of_prop r Hr_contI).
We prove the intermediate
claim Hu_contI0:
continuous_map X Tx I0 T0 (u_of r).
We prove the intermediate
claim Hu_fun:
function_on (u_of r) X I0.
We prove the intermediate
claim HuxI0:
apply_fun (u_of r) x ∈ I0.
An exact proof term for the current goal is (Hu_fun x HxX).
We prove the intermediate
claim HuxR:
apply_fun (u_of r) x ∈ R.
We prove the intermediate
claim HcEq:
c = ((State k) 1) 1.
We prove the intermediate
claim HcR:
c ∈ R.
rewrite the current goal using HcEq (from left to right).
An
exact proof term for the current goal is
(andEL (((State k) 1) 1 ∈ R) (0 < ((State k) 1) 1) (HInv_cpos k HkO)).
rewrite the current goal using Hcomp (from left to right).
rewrite the current goal using HcorrEq (from left to right).
rewrite the current goal using HgNewEval (from left to right).
Let n be given.
An
exact proof term for the current goal is
(HInv_nat n (omega_nat_p n HnO)).
Let x be given.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim H0:
State 0 = BaseState.
An
exact proof term for the current goal is
(nat_primrec_0 BaseState StepState).
rewrite the current goal using H0 (from left to right).
We prove the intermediate
claim HBase:
BaseState = (g0g,(f1s,den)).
rewrite the current goal using HBase (from left to right).
rewrite the current goal using
(tuple_2_0_eq g0g (f1s,den)) (from left to right) at position 1.
rewrite the current goal using
(tuple_2_1_eq g0g (f1s,den)) (from left to right) at position 1.
rewrite the current goal using
(tuple_2_0_eq f1s den) (from left to right) at position 1.
rewrite the current goal using
(tuple_2_1_eq g0g (f1s,den)) (from left to right) at position 1.
rewrite the current goal using
(tuple_2_1_eq f1s den) (from left to right) at position 1.
rewrite the current goal using Hg0g_app (from left to right) at position 1.
An exact proof term for the current goal is (Hf1s_apply x HxA).
rewrite the current goal using Hf1s_app (from left to right) at position 1.
We prove the intermediate
claim Hf1xI2:
apply_fun f1 x ∈ I2.
An exact proof term for the current goal is (Hf1_range x HxA).
rewrite the current goal using HI2def (from left to right).
An exact proof term for the current goal is Hf1xI2.
We prove the intermediate
claim Hf1xR:
apply_fun f1 x ∈ R.
We prove the intermediate
claim Hf1xS:
SNo (apply_fun f1 x).
rewrite the current goal using HmulDiv (from left to right) at position 1.
rewrite the current goal using (Hf1_apply x HxA) (from left to right) at position 1.
We prove the intermediate
claim HfxR:
apply_fun f x ∈ R.
An exact proof term for the current goal is (Hf_R x HxA).
We prove the intermediate
claim Hg0I0:
apply_fun g0 x ∈ I0.
An exact proof term for the current goal is (Hfung0 x HxX).
We prove the intermediate
claim Hg0R:
apply_fun g0 x ∈ R.
rewrite the current goal using
(add_SNo_0R (apply_fun f x) HfxS) (from left to right) at position 1.
Use reflexivity.
Let k be given.
Let x be given.
We prove the intermediate
claim HS:
State (ordsucc k) = StepState k (State k).
An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState k HkNat).
rewrite the current goal using HS (from left to right).
rewrite the current goal using (IH x HxA) (from right to left).
We prove the intermediate
claim HkO:
k ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega k HkNat).
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
Set st to be the term State k.
Set g to be the term
st 0.
Set rpack to be the term
st 1.
Set r to be the term
rpack 0.
Set c to be the term
rpack 1.
Set cNew to be the term
mul_SNo c den.
We prove the intermediate
claim Hdef:
StepState k st = (gNew,(rNew,cNew)).
We prove the intermediate
claim HgStep:
(StepState k st) 0 = gNew.
rewrite the current goal using Hdef (from left to right).
An
exact proof term for the current goal is
(tuple_2_0_eq gNew (rNew,cNew)).
We prove the intermediate
claim HrpackStep:
(StepState k st) 1 = (rNew,cNew).
rewrite the current goal using Hdef (from left to right).
An
exact proof term for the current goal is
(tuple_2_1_eq gNew (rNew,cNew)).
We prove the intermediate
claim HrStep:
((StepState k st) 1) 0 = rNew.
rewrite the current goal using HrpackStep (from left to right).
An
exact proof term for the current goal is
(tuple_2_0_eq rNew cNew).
We prove the intermediate
claim HcStep:
((StepState k st) 1) 1 = cNew.
rewrite the current goal using HrpackStep (from left to right).
An
exact proof term for the current goal is
(tuple_2_1_eq rNew cNew).
rewrite the current goal using HgStep (from left to right) at position 1.
rewrite the current goal using HrStep (from left to right) at position 1.
rewrite the current goal using HcStep (from left to right) at position 1.
We prove the intermediate
claim HgxR:
gx ∈ R.
We prove the intermediate
claim HgEq:
g = (State k) 0.
rewrite the current goal using HgEq (from left to right).
An exact proof term for the current goal is (HInv_g_R_A k HkO x HxA).
We prove the intermediate
claim HgxS:
SNo gx.
An
exact proof term for the current goal is
(real_SNo gx HgxR).
We prove the intermediate
claim HrEq:
r = ((State k) 1) 0.
rewrite the current goal using HrEq (from left to right).
An exact proof term for the current goal is (HInv_r_contI k HkO).
We prove the intermediate
claim Hr_fun:
function_on r A I.
We prove the intermediate
claim HrxI:
rx ∈ I.
An exact proof term for the current goal is (Hr_fun x HxA).
We prove the intermediate
claim HrxR:
rx ∈ R.
We prove the intermediate
claim HrxS:
SNo rx.
An
exact proof term for the current goal is
(real_SNo rx HrxR).
An exact proof term for the current goal is (Hu_of_prop r Hr_contI).
We prove the intermediate
claim Hu_contI0:
continuous_map X Tx I0 T0 (u_of r).
We prove the intermediate
claim Hu_fun:
function_on (u_of r) X I0.
We prove the intermediate
claim HuxI0:
ux ∈ I0.
An exact proof term for the current goal is (Hu_fun x HxX).
We prove the intermediate
claim HuxR:
ux ∈ R.
We prove the intermediate
claim HuxS:
SNo ux.
An
exact proof term for the current goal is
(real_SNo ux HuxR).
We prove the intermediate
claim HcEq:
c = ((State k) 1) 1.
We prove the intermediate
claim HcR:
c ∈ R.
rewrite the current goal using HcEq (from left to right).
An
exact proof term for the current goal is
(andEL (((State k) 1) 1 ∈ R) (0 < ((State k) 1) 1) (HInv_cpos k HkO)).
We prove the intermediate
claim HcS:
SNo c.
An
exact proof term for the current goal is
(real_SNo c HcR).
rewrite the current goal using Hcomp (from left to right).
rewrite the current goal using HcorrEq (from left to right).
An
exact proof term for the current goal is
(real_mul_SNo ux HuxR c HcR).
rewrite the current goal using HgNewEval (from left to right).
rewrite the current goal using HcorrEq (from left to right) at position 1.
Set uxc to be the term
mul_SNo ux c.
We prove the intermediate
claim HuxcR:
uxc ∈ R.
An
exact proof term for the current goal is
(real_mul_SNo ux HuxR c HcR).
We prove the intermediate
claim HuxcS:
SNo uxc.
An
exact proof term for the current goal is
(real_SNo uxc HuxcR).
We prove the intermediate
claim HrNumR:
apply_fun rNum x ∈ R.
rewrite the current goal using HrNumEval (from left to right).
rewrite the current goal using HrNewEq (from left to right).
rewrite the current goal using HrNumEval (from left to right) at position 1.
rewrite the current goal using HnumDef (from right to left) at position 1.
We prove the intermediate
claim HnumR:
num ∈ R.
We prove the intermediate
claim HnumS:
SNo num.
An
exact proof term for the current goal is
(real_SNo num HnumR).
We prove the intermediate
claim HdenS:
SNo den.
An
exact proof term for the current goal is
(real_SNo den HdenR).
We prove the intermediate
claim HdivR:
div_SNo num den ∈ R.
An
exact proof term for the current goal is
(real_div_SNo num HnumR den HdenR).
We prove the intermediate
claim HdivS:
SNo (div_SNo num den).
An
exact proof term for the current goal is
(real_SNo (div_SNo num den) HdivR).
We prove the intermediate
claim HcNewDef:
cNew = mul_SNo c den.
rewrite the current goal using HcNewDef (from left to right).
An
exact proof term for the current goal is
(mul_SNo_assoc (div_SNo num den) c den HdivS HcS HdenS).
rewrite the current goal using HmulAssoc (from left to right).
rewrite the current goal using HmulSwap (from left to right).
We prove the intermediate
claim Hdenne0:
den ≠ 0.
An exact proof term for the current goal is H23ne0.
We prove the intermediate
claim Hcancel:
mul_SNo (div_SNo num den) den = num.
An
exact proof term for the current goal is
(mul_div_SNo_invL num den HnumS HdenS Hdenne0).
rewrite the current goal using Hcancel (from left to right).
rewrite the current goal using HnumEq (from left to right).
We prove the intermediate
claim HuxcDef:
uxc = mul_SNo ux c.
rewrite the current goal using HuxcDef (from left to right) at position 1.
Let n be given.
Let x be given.
An
exact proof term for the current goal is
(HInv_nat n (omega_nat_p n HnO) x HxA).
We prove the intermediate
claim Hfun_g0:
function_on g0 X R.
Set gg to be the term
(λx : set ⇒ apply_fun g0 x).
We prove the intermediate
claim Hgg:
∀x : set, x ∈ X → gg x ∈ R.
Let x be given.
An exact proof term for the current goal is (Hfun_g0 x HxX).
We prove the intermediate
claim Hg0g_def:
g0g = graph X gg.
rewrite the current goal using Hg0g_def (from left to right).
We prove the intermediate
claim H0:
State 0 = BaseState.
An
exact proof term for the current goal is
(nat_primrec_0 BaseState StepState).
rewrite the current goal using H0 (from left to right).
We prove the intermediate
claim HBase:
BaseState = (g0g,(f1s,den)).
rewrite the current goal using HBase (from left to right).
rewrite the current goal using
(tuple_2_0_eq g0g (f1s,den)) (from left to right).
An exact proof term for the current goal is Hg0g_FS.
Let n be given.
We prove the intermediate
claim HS:
State (ordsucc n) = StepState n (State n).
An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState n HnNat).
rewrite the current goal using HS (from left to right).
Set st to be the term State n.
Set g to be the term
st 0.
Set rpack to be the term
st 1.
Set r to be the term
rpack 0.
Set c to be the term
rpack 1.
Set cNew to be the term
mul_SNo c den.
We prove the intermediate
claim HStep0:
(StepState n st) 0 = gNew.
We prove the intermediate
claim Hdef:
StepState n st = (gNew,(rNew,cNew)).
rewrite the current goal using Hdef (from left to right).
An
exact proof term for the current goal is
(tuple_2_0_eq gNew (rNew,cNew)).
rewrite the current goal using HStep0 (from left to right).
We prove the intermediate
claim HnO:
n ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega n HnNat).
We prove the intermediate
claim Hcpack:
((State n) 1) 1 ∈ R ∧ 0 < ((State n) 1) 1.
An exact proof term for the current goal is (HInv_cpos n HnO).
We prove the intermediate
claim Hc_eq:
c = ((State n) 1) 1.
We prove the intermediate
claim HcR0:
((State n) 1) 1 ∈ R.
An
exact proof term for the current goal is
(andEL (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) Hcpack).
We prove the intermediate
claim HcR:
c ∈ R.
rewrite the current goal using Hc_eq (from left to right).
An exact proof term for the current goal is HcR0.
An exact proof term for the current goal is (HInv_r_contI n HnO).
An exact proof term for the current goal is (Hu_of_prop r Hr_contI).
We prove the intermediate
claim Hu_cont:
continuous_map X Tx I0 T0 (u_of r).
We prove the intermediate
claim Hu_fun_I0:
function_on (u_of r) X I0.
We prove the intermediate
claim HI0SubR:
I0 ⊆ R.
We prove the intermediate
claim Hu_fun_R:
function_on (u_of r) X R.
Let x be given.
An
exact proof term for the current goal is
(HI0SubR (apply_fun (u_of r) x) (Hu_fun_I0 x HxX)).
Let n be given.
An
exact proof term for the current goal is
(HInv_nat n (omega_nat_p n HnO)).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let n be given.
We prove the intermediate
claim Hdef:
fn = graph ω (λn0 : set ⇒ (State n0) 0).
rewrite the current goal using
(apply_fun_of_graph_eq fn ω (λn0 : set ⇒ (State n0) 0) n Hdef HnO) (from left to right).
An exact proof term for the current goal is (HInv_g_FS n HnO).
We prove the intermediate
claim HTx':
topology_on X Tx.
We prove the intermediate
claim Hfun_g0:
function_on g0 X R.
We prove the intermediate
claim Hfun_g0g:
function_on g0g X R.
Let x be given.
rewrite the current goal using
(apply_fun_graph X (λx0 : set ⇒ apply_fun g0 x0) x HxX) (from left to right) at position 1.
An exact proof term for the current goal is (Hfun_g0 x HxX).
Let V be given.
We prove the intermediate
claim Hpre_g0:
preimage_of X g0 V ∈ Tx.
Let x be given.
We prove the intermediate
claim HxX:
x ∈ X.
An
exact proof term for the current goal is
(SepE1 X (λy : set ⇒ apply_fun g0g y ∈ V) x Hx).
We prove the intermediate
claim Himg:
apply_fun g0g x ∈ V.
An
exact proof term for the current goal is
(SepE2 X (λy : set ⇒ apply_fun g0g y ∈ V) x Hx).
We prove the intermediate
claim Himg':
apply_fun g0 x ∈ V.
rewrite the current goal using
(apply_fun_graph X (λx0 : set ⇒ apply_fun g0 x0) x HxX) (from right to left) at position 1.
An exact proof term for the current goal is Himg.
An
exact proof term for the current goal is
(SepI X (λy : set ⇒ apply_fun g0 y ∈ V) x HxX Himg').
Let x be given.
We prove the intermediate
claim HxX:
x ∈ X.
An
exact proof term for the current goal is
(SepE1 X (λy : set ⇒ apply_fun g0 y ∈ V) x Hx).
We prove the intermediate
claim Himg:
apply_fun g0 x ∈ V.
An
exact proof term for the current goal is
(SepE2 X (λy : set ⇒ apply_fun g0 y ∈ V) x Hx).
We prove the intermediate
claim Himg':
apply_fun g0g x ∈ V.
rewrite the current goal using
(apply_fun_graph X (λx0 : set ⇒ apply_fun g0 x0) x HxX) (from left to right) at position 1.
An exact proof term for the current goal is Himg.
An
exact proof term for the current goal is
(SepI X (λy : set ⇒ apply_fun g0g y ∈ V) x HxX Himg').
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hpre_g0.
Apply andI to the current goal.
An exact proof term for the current goal is HTx'.
An exact proof term for the current goal is HTR.
Apply andI to the current goal.
An exact proof term for the current goal is Htop.
An exact proof term for the current goal is Hfun_g0g.
Apply andI to the current goal.
An exact proof term for the current goal is Htopfun.
An exact proof term for the current goal is Hpre_g0g.
We prove the intermediate
claim H0:
State 0 = BaseState.
An
exact proof term for the current goal is
(nat_primrec_0 BaseState StepState).
rewrite the current goal using H0 (from left to right).
We prove the intermediate
claim HBase:
BaseState = (g0g,(f1s,den)).
rewrite the current goal using HBase (from left to right).
rewrite the current goal using
(tuple_2_0_eq g0g (f1s,den)) (from left to right).
An exact proof term for the current goal is Hg0g_cont.
Let n be given.
We prove the intermediate
claim HS:
State (ordsucc n) = StepState n (State n).
An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState n HnNat).
rewrite the current goal using HS (from left to right).
Set st to be the term State n.
Set g to be the term
st 0.
Set rpack to be the term
st 1.
Set r to be the term
rpack 0.
Set c to be the term
rpack 1.
Set cNew to be the term
mul_SNo c den.
We prove the intermediate
claim HStep0:
(StepState n st) 0 = gNew.
We prove the intermediate
claim Hdef:
StepState n st = (gNew,(rNew,cNew)).
rewrite the current goal using Hdef (from left to right).
An
exact proof term for the current goal is
(tuple_2_0_eq gNew (rNew,cNew)).
rewrite the current goal using HStep0 (from left to right).
An exact proof term for the current goal is IH.
We prove the intermediate
claim HnO:
n ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega n HnNat).
We prove the intermediate
claim Hcpack:
((State n) 1) 1 ∈ R ∧ 0 < ((State n) 1) 1.
An exact proof term for the current goal is (HInv_cpos n HnO).
We prove the intermediate
claim Hc_eq:
c = ((State n) 1) 1.
We prove the intermediate
claim HcR0:
((State n) 1) 1 ∈ R.
An
exact proof term for the current goal is
(andEL (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) Hcpack).
We prove the intermediate
claim Hcpos0:
0 < ((State n) 1) 1.
An
exact proof term for the current goal is
(andER (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) Hcpack).
We prove the intermediate
claim HcR:
c ∈ R.
rewrite the current goal using Hc_eq (from left to right).
An exact proof term for the current goal is HcR0.
We prove the intermediate
claim Hcpos:
0 < c.
rewrite the current goal using Hc_eq (from left to right).
An exact proof term for the current goal is Hcpos0.
An exact proof term for the current goal is (HInv_r_contI n HnO).
An exact proof term for the current goal is (Hu_of_prop r Hr_contI).
We prove the intermediate
claim Hu_cont:
continuous_map X Tx I0 T0 (u_of r).
We prove the intermediate
claim HI0SubR:
I0 ⊆ R.
rewrite the current goal using HT0 (from left to right).
Let n be given.
An
exact proof term for the current goal is
(HInv_nat n (omega_nat_p n HnO)).
Let n be given.
We prove the intermediate
claim Hdef:
fn = graph ω (λn0 : set ⇒ (State n0) 0).
rewrite the current goal using
(apply_fun_of_graph_eq fn ω (λn0 : set ⇒ (State n0) 0) n Hdef HnO) (from left to right).
An exact proof term for the current goal is (HInv_g_cont n HnO).
We prove the intermediate
claim HInv_g_I:
∀n : set, n ∈ ω → ∀x : set, x ∈ X → apply_fun ((State n) 0) x ∈ I.
Let x be given.
We prove the intermediate
claim H0:
State 0 = BaseState.
An
exact proof term for the current goal is
(nat_primrec_0 BaseState StepState).
rewrite the current goal using H0 (from left to right).
We prove the intermediate
claim HBase:
BaseState = (g0g,(f1s,den)).
rewrite the current goal using HBase (from left to right).
rewrite the current goal using
(tuple_2_0_eq g0g (f1s,den)) (from left to right).
rewrite the current goal using
(tuple_2_0_eq g0g (f1s,den)) (from left to right).
We prove the intermediate
claim Hc0Eq:
((g0g,(f1s,den)) 1) 1 = den.
rewrite the current goal using
(tuple_2_1_eq g0g (f1s,den)) (from left to right) at position 1.
rewrite the current goal using
(tuple_2_1_eq f1s den) (from left to right) at position 1.
Use reflexivity.
Apply andI to the current goal.
We prove the intermediate
claim Hg0xI0:
apply_fun g0 x ∈ I0.
An exact proof term for the current goal is (Hfung0 x HxX).
We prove the intermediate
claim Hg0xI0:
apply_fun g0 x ∈ I0.
An exact proof term for the current goal is (Hfung0 x HxX).
We prove the intermediate
claim HdenDef:
den = two_thirds.
rewrite the current goal using Hc0Eq (from left to right).
rewrite the current goal using HdenDef (from left to right).
rewrite the current goal using Hc0Eq (from left to right).
rewrite the current goal using HdenDef (from left to right).
rewrite the current goal using HlowEq0 (from left to right).
rewrite the current goal using HupEq0 (from left to right).
An exact proof term for the current goal is Hg0xI0.
Let n be given.
Let x be given.
We prove the intermediate
claim HSnat:
State (ordsucc n) = StepState n (State n).
An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState n HnNat).
rewrite the current goal using HSnat (from left to right).
Set st to be the term State n.
Set g to be the term
st 0.
Set rpack to be the term
st 1.
Set r to be the term
rpack 0.
Set c to be the term
rpack 1.
Set cNew to be the term
mul_SNo c den.
We prove the intermediate
claim HdefStep:
StepState n st = (gNew,(rNew,cNew)).
rewrite the current goal using HdefStep (from left to right).
We prove the intermediate
claim HgStep:
((gNew,(rNew,cNew)) 0) = gNew.
An
exact proof term for the current goal is
(tuple_2_0_eq gNew (rNew,cNew)).
rewrite the current goal using HgStep (from left to right).
We prove the intermediate
claim HnO:
n ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega n HnNat).
We prove the intermediate
claim HrEq:
r = ((State n) 1) 0.
We prove the intermediate
claim HcEq:
c = ((State n) 1) 1.
rewrite the current goal using HrEq (from left to right).
An exact proof term for the current goal is (HInv_r_contI n HnO).
An exact proof term for the current goal is (Hu_of_prop r Hr_contI).
We prove the intermediate
claim Hu_contI0:
continuous_map X Tx I0 T0 (u_of r).
We prove the intermediate
claim Hu_fun:
function_on (u_of r) X I0.
We prove the intermediate
claim HuxI0:
apply_fun (u_of r) x ∈ I0.
An exact proof term for the current goal is (Hu_fun x HxX).
We prove the intermediate
claim HuxR:
apply_fun (u_of r) x ∈ R.
We prove the intermediate
claim HcR:
c ∈ R.
rewrite the current goal using HcEq (from left to right).
An
exact proof term for the current goal is
(andEL (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) (HInv_cpos n HnO)).
We prove the intermediate
claim HgEq:
g = (State n) 0.
We prove the intermediate
claim HgxI:
apply_fun g x ∈ I.
rewrite the current goal using HgEq (from left to right).
We prove the intermediate
claim HgxR:
apply_fun g x ∈ R.
rewrite the current goal using Hcomp (from left to right).
rewrite the current goal using HcorrEq (from left to right).
rewrite the current goal using HgNewEval (from left to right).
rewrite the current goal using HcorrEq (from left to right).
We prove the intermediate
claim Hcpos:
0 < c.
rewrite the current goal using HcEq (from left to right).
An
exact proof term for the current goal is
(andER (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) (HInv_cpos n HnO)).
rewrite the current goal using HgEq (from left to right).
rewrite the current goal using HcEq (from left to right).
We prove the intermediate
claim HuS:
SNo (apply_fun (u_of r) x).
We prove the intermediate
claim HcS:
SNo c.
An
exact proof term for the current goal is
(real_SNo c HcR).
An exact proof term for the current goal is Hle.
An exact proof term for the current goal is Hle.
We prove the intermediate
claim H0le_c:
0 ≤ c.
An
exact proof term for the current goal is
(SNoLtLe 0 c Hcpos).
rewrite the current goal using HhiEq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HhiEq (from right to left).
An exact proof term for the current goal is HmulLeHi.
rewrite the current goal using HloEq (from right to left) at position 1.
An exact proof term for the current goal is HmulLeLo.
Apply andI to the current goal.
We prove the intermediate
claim HtR:
t ∈ R.
We prove the intermediate
claim Htpos:
0 < t.
We prove the intermediate
claim HcS:
SNo c.
An
exact proof term for the current goal is
(real_SNo c HcR).
We prove the intermediate
claim H0lt_t:
Rlt 0 t.
An
exact proof term for the current goal is
(RltI 0 t real_0 HtR Htpos).
We prove the intermediate
claim H0le_t:
Rle 0 t.
An exact proof term for the current goal is Htmp.
We prove the intermediate
claim H10Eq:
add_SNo 1 0 = 1.
rewrite the current goal using H10Eq (from left to right) at position 1.
We prove the intermediate
claim HdenDef:
den = two_thirds.
rewrite the current goal using HdenDef (from left to right).
Use reflexivity.
We prove the intermediate
claim HcPairEq:
((gNew,(rNew,cNew)) 1) 1 = cNew.
We prove the intermediate
claim Hinner:
((gNew,(rNew,cNew)) 1) = (rNew,cNew).
An
exact proof term for the current goal is
(tuple_2_1_eq gNew (rNew,cNew)).
rewrite the current goal using Hinner (from left to right) at position 1.
An
exact proof term for the current goal is
(tuple_2_1_eq rNew cNew).
rewrite the current goal using HcPairEq (from left to right).
rewrite the current goal using HcNewEq (from left to right).
Use reflexivity.
rewrite the current goal using HcGoalEq (from left to right).
Use reflexivity.
rewrite the current goal using HcGoalEq (from left to right).
Use reflexivity.
rewrite the current goal using HlowEq (from left to right).
rewrite the current goal using HupEq (from left to right).
An exact proof term for the current goal is HsumShrink.
Let n be given.
Let x be given.
Let n be given.
Let x be given.
We prove the intermediate
claim Hdef:
fn = graph ω (λn0 : set ⇒ (State n0) 0).
rewrite the current goal using
(apply_fun_of_graph_eq fn ω (λn0 : set ⇒ (State n0) 0) n Hdef HnO) (from left to right).
An exact proof term for the current goal is (HInv_g_I n HnO x HxX).
Let x be given.
We prove the intermediate
claim HseqEq:
seq1 = seq2.
Let p be given.
Let n be given.
rewrite the current goal using HpEq (from left to right).
We prove the intermediate
claim Hdef:
fn = graph ω (λn0 : set ⇒ (State n0) 0).
rewrite the current goal using
(apply_fun_of_graph_eq fn ω (λn0 : set ⇒ (State n0) 0) n Hdef HnO) (from left to right) at position 1.
An
exact proof term for the current goal is
(ReplI ω (λn0 : set ⇒ (n0,apply_fun ((State n0) 0) x)) n HnO).
Let p be given.
Let n be given.
rewrite the current goal using HpEq (from left to right).
We prove the intermediate
claim Hdef:
fn = graph ω (λn0 : set ⇒ (State n0) 0).
rewrite the current goal using
(apply_fun_of_graph_eq fn ω (λn0 : set ⇒ (State n0) 0) n Hdef HnO) (from right to left) at position 1.
rewrite the current goal using Hseq1def (from right to left).
rewrite the current goal using HseqEq (from left to right).
We prove the intermediate
claim Hseq2On:
sequence_on seq2 R.
Let n be given.
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim Hseq2def:
seq2 = graph ω (λn0 : set ⇒ apply_fun ((State n0) 0) x).
rewrite the current goal using Hseq2def (from left to right).
We prove the intermediate
claim HgR_nat:
∀k : set, nat_p k → apply_fun ((State k) 0) x ∈ R.
We prove the intermediate
claim H0:
State 0 = BaseState.
An
exact proof term for the current goal is
(nat_primrec_0 BaseState StepState).
rewrite the current goal using H0 (from left to right).
We prove the intermediate
claim HBase:
BaseState = (g0g,(f1s,den)).
rewrite the current goal using HBase (from left to right).
rewrite the current goal using
(tuple_2_0_eq g0g (f1s,den)) (from left to right).
We prove the intermediate
claim HxX0:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim Hg0I0:
apply_fun g0 x ∈ I0.
An exact proof term for the current goal is (Hfung0 x HxX0).
Let k be given.
We prove the intermediate
claim HS:
State (ordsucc k) = StepState k (State k).
An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState k HkNat).
rewrite the current goal using HS (from left to right).
Set st to be the term State k.
Set g to be the term
st 0.
Set rpack to be the term
st 1.
Set r to be the term
rpack 0.
Set c to be the term
rpack 1.
Set cNew to be the term
mul_SNo c den.
We prove the intermediate
claim Hdef:
StepState k st = (gNew,(rNew,cNew)).
We prove the intermediate
claim HgStep:
(StepState k st) 0 = gNew.
rewrite the current goal using Hdef (from left to right).
An
exact proof term for the current goal is
(tuple_2_0_eq gNew (rNew,cNew)).
rewrite the current goal using HgStep (from left to right).
We prove the intermediate
claim HxX0:
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
We prove the intermediate
claim HgEq:
g = (State k) 0.
We prove the intermediate
claim HgxR:
apply_fun g x ∈ R.
rewrite the current goal using HgEq (from left to right).
An exact proof term for the current goal is IHk.
We prove the intermediate
claim HkO:
k ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega k HkNat).
We prove the intermediate
claim HrEq:
r = ((State k) 1) 0.
rewrite the current goal using HrEq (from left to right).
An exact proof term for the current goal is (HInv_r_contI k HkO).
An exact proof term for the current goal is (Hu_of_prop r Hr_contI).
We prove the intermediate
claim Hu_contI0:
continuous_map X Tx I0 T0 (u_of r).
We prove the intermediate
claim Hu_fun:
function_on (u_of r) X I0.
We prove the intermediate
claim HuxI0:
apply_fun (u_of r) x ∈ I0.
An exact proof term for the current goal is (Hu_fun x HxX0).
We prove the intermediate
claim HuxR:
apply_fun (u_of r) x ∈ R.
We prove the intermediate
claim HcEq:
c = ((State k) 1) 1.
We prove the intermediate
claim HcR:
c ∈ R.
rewrite the current goal using HcEq (from left to right).
An
exact proof term for the current goal is
(andEL (((State k) 1) 1 ∈ R) (0 < ((State k) 1) 1) (HInv_cpos k HkO)).
rewrite the current goal using Hcomp (from left to right).
rewrite the current goal using HcorrEq (from left to right).
rewrite the current goal using HgNewEval (from left to right).
An
exact proof term for the current goal is
(HgR_nat n (omega_nat_p n HnO)).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hseq2On.
We prove the intermediate
claim HlimR:
lim ∈ R.
An exact proof term for the current goal is (Hf_R x HxA).
An exact proof term for the current goal is HlimR.
Let eps be given.
We prove the intermediate
claim HepsR:
eps ∈ R.
An
exact proof term for the current goal is
(andEL (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate
claim HepsPos:
Rlt 0 eps.
An
exact proof term for the current goal is
(andER (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate
claim HepsS:
SNo eps.
An
exact proof term for the current goal is
(real_SNo eps HepsR).
We prove the intermediate
claim HepsLt1:
Rlt eps 1.
An
exact proof term for the current goal is
(RltI eps 1 HepsR real_1 HepsLt1S).
We prove the intermediate
claim Hex_c_small:
∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → ((State n) 1) 1 < eps.
We prove the intermediate
claim HexK:
∃K ∈ ω, eps_ K < eps.
Apply HexK to the current goal.
Let K be given.
Assume HK.
We prove the intermediate
claim HKomega:
K ∈ ω.
An
exact proof term for the current goal is
(andEL (K ∈ ω) (eps_ K < eps) HK).
We prove the intermediate
claim HepsKltEpsS:
eps_ K < eps.
An
exact proof term for the current goal is
(andER (K ∈ ω) (eps_ K < eps) HK).
We prove the intermediate
claim HepsKR:
eps_ K ∈ R.
We prove the intermediate
claim HepsKltEps:
Rlt (eps_ K) eps.
An
exact proof term for the current goal is
(RltI (eps_ K) eps HepsKR HepsR HepsKltEpsS).
We prove the intermediate
claim HexN:
∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → ((State n) 1) 1 < eps_ K.
We prove the intermediate
claim HKnat:
nat_p K.
An
exact proof term for the current goal is
(omega_nat_p K HKomega).
An
exact proof term for the current goal is
(nat_inv K HKnat).
Apply HKcase to the current goal.
We use
0 to
witness the existential quantifier.
Apply andI to the current goal.
Let n be given.
We will
prove ((State n) 1) 1 < eps_ K.
rewrite the current goal using HK0 (from left to right).
rewrite the current goal using
eps_0_1 (from left to right).
An exact proof term for the current goal is (HInv_c_lt1 n HnO).
Apply Hexk to the current goal.
Let k be given.
We prove the intermediate
claim HkNat:
nat_p k.
We prove the intermediate
claim HKeq:
K = ordsucc k.
We use N0 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate
claim HN0O:
N0 ∈ ω.
rewrite the current goal using
(add_nat_add_SNo K HKomega K HKomega) (from left to right).
An
exact proof term for the current goal is
(add_SNo_In_omega K HKomega K HKomega).
An exact proof term for the current goal is HN0O.
Let n be given.
We prove the intermediate
claim HKnat:
nat_p K.
An
exact proof term for the current goal is
(omega_nat_p K HKomega).
We prove the intermediate
claim HdenS:
SNo den.
An
exact proof term for the current goal is
(real_SNo den HdenR).
We prove the intermediate
claim HdenDef:
den = two_thirds.
We prove the intermediate
claim HdenLt1:
den < 1.
rewrite the current goal using HdenDef (from left to right).
Set den2 to be the term
mul_SNo den den.
We prove the intermediate
claim Hden2S:
SNo den2.
An
exact proof term for the current goal is
(SNo_mul_SNo den den HdenS HdenS).
We prove the intermediate
claim Hden2Lt_eps1:
den2 < eps_ 1.
rewrite the current goal using HdenDef (from left to right) at position 1.
rewrite the current goal using HdenDef (from left to right) at position 2.
Let m be given.
We prove the intermediate
claim HS:
State (ordsucc m) = StepState m (State m).
An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState m HmNat).
rewrite the current goal using HS (from left to right).
Set st to be the term State m.
Set g to be the term
st 0.
Set rpack to be the term
st 1.
Set r to be the term
rpack 0.
Set c to be the term
rpack 1.
Set cNew to be the term
mul_SNo c den.
We prove the intermediate
claim Hdef:
StepState m st = (gNew,(rNew,cNew)).
We prove the intermediate
claim HtEq:
((StepState m st) 1) 1 = cNew.
We prove the intermediate
claim Hinner:
(StepState m st) 1 = (rNew,cNew).
rewrite the current goal using Hdef (from left to right).
An
exact proof term for the current goal is
(tuple_2_1_eq gNew (rNew,cNew)).
rewrite the current goal using Hinner (from left to right).
An
exact proof term for the current goal is
(tuple_2_1_eq rNew cNew).
rewrite the current goal using HtEq (from left to right).
We prove the intermediate
claim HcEq:
c = ((State m) 1) 1.
rewrite the current goal using HcEq (from left to right).
Use reflexivity.
We prove the intermediate
claim Hc_succ_lt:
∀t : set, t ∈ ω → ((State (ordsucc t)) 1) 1 < ((State t) 1) 1.
Let t be given.
We prove the intermediate
claim HtNat:
nat_p t.
An
exact proof term for the current goal is
(omega_nat_p t HtO).
We prove the intermediate
claim HcEq:
((State (ordsucc t)) 1) 1 = mul_SNo (((State t) 1) 1) den.
An exact proof term for the current goal is (Hc_step t HtNat).
rewrite the current goal using HcEq (from left to right).
We prove the intermediate
claim HctR:
((State t) 1) 1 ∈ R.
An
exact proof term for the current goal is
(andEL (((State t) 1) 1 ∈ R) (0 < ((State t) 1) 1) (HInv_cpos t HtO)).
We prove the intermediate
claim HctS:
SNo (((State t) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State t) 1) 1) HctR).
We prove the intermediate
claim HctPos:
0 < (((State t) 1) 1).
An
exact proof term for the current goal is
(andER (((State t) 1) 1 ∈ R) (0 < ((State t) 1) 1) (HInv_cpos t HtO)).
We prove the intermediate
claim HmulLt:
mul_SNo den (((State t) 1) 1) < ((State t) 1) 1.
An
exact proof term for the current goal is
(mul_SNo_Lt1_pos_Lt den (((State t) 1) 1) HdenS HctS HdenLt1 HctPos).
We prove the intermediate
claim HmulEq:
mul_SNo den (((State t) 1) 1) = mul_SNo (((State t) 1) 1) den.
An
exact proof term for the current goal is
(mul_SNo_com den (((State t) 1) 1) HdenS HctS).
rewrite the current goal using HmulEq (from right to left).
An exact proof term for the current goal is HmulLt.
We prove the intermediate
claim Hc_even_lt:
∀t : set, nat_p t → ((State (add_nat t t)) 1) 1 < eps_ t.
rewrite the current goal using
(add_nat_0R 0) (from left to right) at position 1.
rewrite the current goal using
eps_0_1 (from left to right).
Let t be given.
We prove the intermediate
claim HNnat:
nat_p N.
An
exact proof term for the current goal is
(add_nat_p t HtNat t HtNat).
rewrite the current goal using
(add_nat_SR t t HtNat) (from left to right).
Use reflexivity.
rewrite the current goal using Hidx (from left to right).
We prove the intermediate
claim HN0:
N ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega N HNnat).
We prove the intermediate
claim HcSN:
((State (ordsucc N)) 1) 1 = mul_SNo (((State N) 1) 1) den.
An exact proof term for the current goal is (Hc_step N HNnat).
An
exact proof term for the current goal is
(nat_ordsucc N HNnat).
rewrite the current goal using
(Hc_step (ordsucc N) HSNnat) (from left to right).
rewrite the current goal using HcSN (from left to right).
Use reflexivity.
rewrite the current goal using HcSSN (from left to right).
rewrite the current goal using
(mul_SNo_assoc (((State N) 1) 1) den den (real_SNo (((State N) 1) 1) (andEL (((State N) 1) 1 ∈ R) (0 < ((State N) 1) 1) (HInv_cpos N HN0))) HdenS HdenS) (from right to left).
We prove the intermediate
claim Hden2Def:
den2 = mul_SNo den den.
rewrite the current goal using Hden2Def (from right to left).
We prove the intermediate
claim HcNpos:
0 < ((State N) 1) 1.
An
exact proof term for the current goal is
(andER (((State N) 1) 1 ∈ R) (0 < ((State N) 1) 1) (HInv_cpos N HN0)).
We prove the intermediate
claim HcNS:
SNo (((State N) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State N) 1) 1) (andEL (((State N) 1) 1 ∈ R) (0 < ((State N) 1) 1) (HInv_cpos N HN0))).
rewrite the current goal using
(mul_SNo_com (((State N) 1) 1) den2 HcNS Hden2S) (from left to right).
We prove the intermediate
claim Heps1R:
(eps_ 1) ∈ R.
We prove the intermediate
claim Heps1S:
SNo (eps_ 1).
An
exact proof term for the current goal is
(real_SNo (eps_ 1) Heps1R).
We prove the intermediate
claim Heps1pos:
0 < eps_ 1.
An
exact proof term for the current goal is
(pos_mul_SNo_Lt' den2 (eps_ 1) (((State N) 1) 1) Hden2S Heps1S HcNS HcNpos Hden2Lt_eps1).
We prove the intermediate
claim Heps_tR:
(eps_ t) ∈ R.
We prove the intermediate
claim Heps_tS:
SNo (eps_ t).
An
exact proof term for the current goal is
(real_SNo (eps_ t) Heps_tR).
An
exact proof term for the current goal is
(mul_SNo_com (eps_ 1) (((State N) 1) 1) Heps1S HcNS).
rewrite the current goal using HcomL (from left to right).
rewrite the current goal using HcomR (from left to right).
An
exact proof term for the current goal is
(pos_mul_SNo_Lt' (((State N) 1) 1) (eps_ t) (eps_ 1) HcNS Heps_tS Heps1S Heps1pos IH).
We prove the intermediate
claim Hordt:
ordinal t.
An
exact proof term for the current goal is
(nat_p_ordinal t HtNat).
Use reflexivity.
rewrite the current goal using HepsEq (from right to left).
An exact proof term for the current goal is HmulTra.
We prove the intermediate
claim HcN0:
((State N0) 1) 1 < eps_ K.
An exact proof term for the current goal is (Hc_even_lt K HKnat).
We prove the intermediate
claim HnNat:
nat_p n.
An
exact proof term for the current goal is
(omega_nat_p n HnO).
We prove the intermediate
claim HN0O:
N0 ∈ ω.
rewrite the current goal using
(add_nat_add_SNo K HKomega K HKomega) (from left to right).
An
exact proof term for the current goal is
(add_SNo_In_omega K HKomega K HKomega).
We prove the intermediate
claim HN0Nat:
nat_p N0.
An
exact proof term for the current goal is
(omega_nat_p N0 HN0O).
We prove the intermediate
claim Hexk:
∃k : set, nat_p k ∧ n = add_nat k N0.
An
exact proof term for the current goal is
(nat_Subq_add_ex N0 HN0Nat n HnNat HN0sub).
Apply Hexk to the current goal.
Let k1 be given.
Assume Hk1.
We prove the intermediate
claim Hk1Nat:
nat_p k1.
We prove the intermediate
claim HnEq:
n = add_nat k1 N0.
rewrite the current goal using HnEq (from left to right).
An
exact proof term for the current goal is
(nat_inv k1 Hk1Nat).
Apply Hkcase to the current goal.
rewrite the current goal using Hk10 (from left to right).
rewrite the current goal using
(add_nat_0L N0 HN0Nat) (from left to right).
An exact proof term for the current goal is HcN0.
Apply Hk1S to the current goal.
Let j be given.
Assume Hj.
We prove the intermediate
claim HjNat:
nat_p j.
We prove the intermediate
claim Hk1Eq:
k1 = ordsucc j.
rewrite the current goal using Hk1Eq (from left to right).
rewrite the current goal using
(add_nat_SL 0 nat_0 N0 HN0Nat) (from left to right).
rewrite the current goal using
(add_nat_0L N0 HN0Nat) (from left to right).
An exact proof term for the current goal is (Hc_succ_lt N0 HN0O).
Let j be given.
We prove the intermediate
claim HcR0:
((State N0) 1) 1 ∈ R.
An
exact proof term for the current goal is
(andEL (((State N0) 1) 1 ∈ R) (0 < ((State N0) 1) 1) (HInv_cpos N0 HN0O)).
We prove the intermediate
claim HcS0:
SNo (((State N0) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State N0) 1) 1) HcR0).
We prove the intermediate
claim HltN0:
((State (add_nat (ordsucc j) N0)) 1) 1 < ((State N0) 1) 1.
An exact proof term for the current goal is (Hdec j HjNat).
We prove the intermediate
claim HN0R:
((State N0) 1) 1 ∈ R.
An
exact proof term for the current goal is
(andEL (((State N0) 1) 1 ∈ R) (0 < ((State N0) 1) 1) (HInv_cpos N0 HN0O)).
We prove the intermediate
claim HN0S:
SNo (((State N0) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State N0) 1) 1) HN0R).
We prove the intermediate
claim HepsKS:
SNo (eps_ K).
An
exact proof term for the current goal is
(real_SNo (eps_ K) HepsKR).
Apply HexN to the current goal.
Let N be given.
Assume HN.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
(andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → ((State n) 1) 1 < eps_ K) HN).
Let n be given.
We prove the intermediate
claim HNprop:
∀t : set, t ∈ ω → N ⊆ t → ((State t) 1) 1 < eps_ K.
An
exact proof term for the current goal is
(andER (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → ((State n) 1) 1 < eps_ K) HN).
We prove the intermediate
claim HcLtEpsK:
((State n) 1) 1 < eps_ K.
An exact proof term for the current goal is (HNprop n HnO HNsub).
We prove the intermediate
claim HcR:
((State n) 1) 1 ∈ R.
An
exact proof term for the current goal is
(andEL (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) (HInv_cpos n HnO)).
We prove the intermediate
claim HcS:
SNo (((State n) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State n) 1) 1) HcR).
We prove the intermediate
claim HepsKS:
SNo (eps_ K).
An
exact proof term for the current goal is
(real_SNo (eps_ K) HepsKR).
We prove the intermediate
claim HepsS0:
SNo eps.
An
exact proof term for the current goal is
(real_SNo eps HepsR).
An
exact proof term for the current goal is
(SNoLt_tra (((State n) 1) 1) (eps_ K) eps HcS HepsKS HepsS0 HcLtEpsK HepsKltEpsS).
Apply Hex_c_small to the current goal.
Let N be given.
Assume HNpair.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An
exact proof term for the current goal is
(andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → ((State n) 1) 1 < eps) HNpair).
Let n be given.
We prove the intermediate
claim Hseq2nR:
apply_fun seq2 n ∈ R.
An exact proof term for the current goal is (Hseq2On n HnO).
We prove the intermediate
claim HlimR:
lim ∈ R.
An exact proof term for the current goal is (Hf_R x HxA).
rewrite the current goal using HdefM (from left to right).
Set b to be the term lim.
We prove the intermediate
claim HtR:
t ∈ R.
We prove the intermediate
claim HtS:
SNo t.
An
exact proof term for the current goal is
(real_SNo t HtR).
We prove the intermediate
claim HaS:
SNo a.
An
exact proof term for the current goal is
(real_SNo a Hseq2nR).
We prove the intermediate
claim HbS:
SNo b.
An
exact proof term for the current goal is
(real_SNo b HlimR).
We prove the intermediate
claim HaEq:
a = apply_fun ((State n) 0) x.
We prove the intermediate
claim Hseq2def:
seq2 = graph ω (λn0 : set ⇒ apply_fun ((State n0) 0) x).
rewrite the current goal using Hseq2def (from left to right).
Use reflexivity.
rewrite the current goal using HaEq (from left to right).
An exact proof term for the current goal is (HInv_residual_identity_A n HnO x HxA).
rewrite the current goal using Hident (from right to left) at position 1.
We prove the intermediate
claim HrcR:
rc ∈ R.
We prove the intermediate
claim Hrfun:
continuous_map A Ta I Ti (((State n) 1) 0).
An exact proof term for the current goal is (HInv_r_contI n HnO).
We prove the intermediate
claim Hrfun_on:
function_on (((State n) 1) 0) A I.
We prove the intermediate
claim HrxI:
apply_fun (((State n) 1) 0) x ∈ I.
An exact proof term for the current goal is (Hrfun_on x HxA).
We prove the intermediate
claim HrxR:
apply_fun (((State n) 1) 0) x ∈ R.
We prove the intermediate
claim HcR:
((State n) 1) 1 ∈ R.
An
exact proof term for the current goal is
(andEL (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) (HInv_cpos n HnO)).
We prove the intermediate
claim HrcS:
SNo rc.
An
exact proof term for the current goal is
(real_SNo rc HrcR).
We prove the intermediate
claim HaS0:
SNo a.
An
exact proof term for the current goal is
(real_SNo a Hseq2nR).
rewrite the current goal using
(add_SNo_com a rc HaS0 HrcS) (from left to right) at position 1.
We prove the intermediate
claim HcR:
((State n) 1) 1 ∈ R.
An
exact proof term for the current goal is
(andEL (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) (HInv_cpos n HnO)).
We prove the intermediate
claim HcS:
SNo (((State n) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State n) 1) 1) HcR).
We prove the intermediate
claim HcLtEps:
((State n) 1) 1 < eps.
An
exact proof term for the current goal is
(andER (N ∈ ω) (∀n0 : set, n0 ∈ ω → N ⊆ n0 → ((State n0) 1) 1 < eps) HNpair n HnO HNsub).
We prove the intermediate
claim Hcpos:
0 < ((State n) 1) 1.
An
exact proof term for the current goal is
(andER (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) (HInv_cpos n HnO)).
We prove the intermediate
claim H0le_c:
0 ≤ ((State n) 1) 1.
An
exact proof term for the current goal is
(SNoLtLe 0 (((State n) 1) 1) Hcpos).
We prove the intermediate
claim Hrfun:
continuous_map A Ta I Ti (((State n) 1) 0).
An exact proof term for the current goal is (HInv_r_contI n HnO).
We prove the intermediate
claim Hrfun_on:
function_on (((State n) 1) 0) A I.
We prove the intermediate
claim HrxI:
apply_fun (((State n) 1) 0) x ∈ I.
An exact proof term for the current goal is (Hrfun_on x HxA).
We prove the intermediate
claim HrxR:
apply_fun (((State n) 1) 0) x ∈ R.
We prove the intermediate
claim Hmcr:
(minus_SNo (((State n) 1) 1)) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo (((State n) 1) 1) HcR).
We prove the intermediate
claim HhiLe:
mul_SNo (apply_fun (((State n) 1) 0) x) (((State n) 1) 1) ≤ ((State n) 1) 1.
We prove the intermediate
claim HabstLtEps:
abs_SNo t < eps.
rewrite the current goal using HabsEq (from left to right).
rewrite the current goal using HrcEq (from left to right).
An exact proof term for the current goal is HabsLtEps.
rewrite the current goal using HepsEq1 (from left to right).
We use
0 to
witness the existential quantifier.
Apply andI to the current goal.
Let n be given.
We prove the intermediate
claim Hseq2nR:
apply_fun seq2 n ∈ R.
An exact proof term for the current goal is (Hseq2On n HnO).
We prove the intermediate
claim HlimR:
lim ∈ R.
An exact proof term for the current goal is (Hf_R x HxA).
rewrite the current goal using HdefM (from left to right).
Set b to be the term lim.
We prove the intermediate
claim HtR:
t ∈ R.
We prove the intermediate
claim HtS:
SNo t.
An
exact proof term for the current goal is
(real_SNo t HtR).
We prove the intermediate
claim HaS:
SNo a.
An
exact proof term for the current goal is
(real_SNo a Hseq2nR).
We prove the intermediate
claim HbS:
SNo b.
An
exact proof term for the current goal is
(real_SNo b HlimR).
We prove the intermediate
claim HaEq:
a = apply_fun ((State n) 0) x.
We prove the intermediate
claim Hseq2def:
seq2 = graph ω (λn0 : set ⇒ apply_fun ((State n0) 0) x).
rewrite the current goal using Hseq2def (from left to right).
Use reflexivity.
rewrite the current goal using HaEq (from left to right).
An exact proof term for the current goal is (HInv_residual_identity_A n HnO x HxA).
rewrite the current goal using Hident (from right to left) at position 1.
We prove the intermediate
claim HrcR:
rc ∈ R.
We prove the intermediate
claim Hrfun:
continuous_map A Ta I Ti (((State n) 1) 0).
An exact proof term for the current goal is (HInv_r_contI n HnO).
We prove the intermediate
claim Hrfun_on:
function_on (((State n) 1) 0) A I.
We prove the intermediate
claim HrxI:
apply_fun (((State n) 1) 0) x ∈ I.
An exact proof term for the current goal is (Hrfun_on x HxA).
We prove the intermediate
claim HrxR:
apply_fun (((State n) 1) 0) x ∈ R.
We prove the intermediate
claim HcR:
((State n) 1) 1 ∈ R.
An
exact proof term for the current goal is
(andEL (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) (HInv_cpos n HnO)).
We prove the intermediate
claim HrcS:
SNo rc.
An
exact proof term for the current goal is
(real_SNo rc HrcR).
We prove the intermediate
claim HaS0:
SNo a.
An
exact proof term for the current goal is
(real_SNo a Hseq2nR).
rewrite the current goal using
(add_SNo_com a rc HaS0 HrcS) (from left to right) at position 1.
We prove the intermediate
claim HcR:
((State n) 1) 1 ∈ R.
An
exact proof term for the current goal is
(andEL (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) (HInv_cpos n HnO)).
We prove the intermediate
claim HcS:
SNo (((State n) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State n) 1) 1) HcR).
We prove the intermediate
claim HcLt1:
((State n) 1) 1 < 1.
An exact proof term for the current goal is (HInv_c_lt1 n HnO).
We prove the intermediate
claim Hcpos:
0 < ((State n) 1) 1.
An
exact proof term for the current goal is
(andER (((State n) 1) 1 ∈ R) (0 < ((State n) 1) 1) (HInv_cpos n HnO)).
We prove the intermediate
claim H0le_c:
0 ≤ ((State n) 1) 1.
An
exact proof term for the current goal is
(SNoLtLe 0 (((State n) 1) 1) Hcpos).
We prove the intermediate
claim Hrfun:
continuous_map A Ta I Ti (((State n) 1) 0).
An exact proof term for the current goal is (HInv_r_contI n HnO).
We prove the intermediate
claim Hrfun_on:
function_on (((State n) 1) 0) A I.
We prove the intermediate
claim HrxI:
apply_fun (((State n) 1) 0) x ∈ I.
An exact proof term for the current goal is (Hrfun_on x HxA).
We prove the intermediate
claim HrxR:
apply_fun (((State n) 1) 0) x ∈ R.
We prove the intermediate
claim HrxS:
SNo (apply_fun (((State n) 1) 0) x).
We prove the intermediate
claim Hmcr:
(minus_SNo (((State n) 1) 1)) ∈ R.
An
exact proof term for the current goal is
(real_minus_SNo (((State n) 1) 1) HcR).
We prove the intermediate
claim HhiLe:
mul_SNo (apply_fun (((State n) 1) 0) x) (((State n) 1) 1) ≤ ((State n) 1) 1.
We prove the intermediate
claim HabstLt1:
Rlt (abs_SNo t) 1.
rewrite the current goal using HabsEq (from left to right).
rewrite the current goal using HrcEq (from left to right).
An exact proof term for the current goal is HabsLt1R.
rewrite the current goal using Hbddef (from left to right).
An exact proof term for the current goal is HabstLt1.
We prove the intermediate
claim H1LtEps:
Rlt 1 eps.
An
exact proof term for the current goal is
(RltI 1 eps real_1 HepsR H1LtEpsS).
We use
0 to
witness the existential quantifier.
Apply andI to the current goal.
Let n be given.
We prove the intermediate
claim Hseq2nR:
apply_fun seq2 n ∈ R.
An exact proof term for the current goal is (Hseq2On n HnO).
We prove the intermediate
claim HlimR:
lim ∈ R.
An exact proof term for the current goal is (Hf_R x HxA).
rewrite the current goal using HdefM (from left to right).
An exact proof term for the current goal is Hseq2_conv.
Let eps be given.
We prove the intermediate
claim HepsS:
SNo eps.
An
exact proof term for the current goal is
(real_SNo eps HepsR).
Let eps0 be given.
We prove the intermediate
claim Heps0S:
SNo eps0.
An
exact proof term for the current goal is
(real_SNo eps0 Heps0R).
We prove the intermediate
claim HetaR:
eta ∈ R.
We prove the intermediate
claim HetaS:
SNo eta.
An
exact proof term for the current goal is
(real_SNo eta HetaR).
We prove the intermediate
claim Heps0PosS:
0 < eps0.
An
exact proof term for the current goal is
(RltE_lt 0 eps0 Heps0Pos).
We prove the intermediate
claim Heps1S:
SNo (eps_ 1).
We prove the intermediate
claim Heps1PosS:
0 < eps_ 1.
We prove the intermediate
claim HetaPosS:
0 < eta.
An
exact proof term for the current goal is
(mul_SNo_pos_pos eps0 (eps_ 1) Heps0S Heps1S Heps0PosS Heps1PosS).
We prove the intermediate
claim HetaPos:
Rlt 0 eta.
An
exact proof term for the current goal is
(RltI 0 eta real_0 HetaR HetaPosS).
We prove the intermediate
claim HexK:
∃K ∈ ω, eps_ K < eta.
Apply HexK to the current goal.
Let K be given.
Assume HK.
We prove the intermediate
claim HKomega:
K ∈ ω.
An
exact proof term for the current goal is
(andEL (K ∈ ω) (eps_ K < eta) HK).
We prove the intermediate
claim HKnat:
nat_p K.
An
exact proof term for the current goal is
(omega_nat_p K HKomega).
We prove the intermediate
claim HepsKltEtaS:
eps_ K < eta.
An
exact proof term for the current goal is
(andER (K ∈ ω) (eps_ K < eta) HK).
We prove the intermediate
claim HepsKR:
eps_ K ∈ R.
We prove the intermediate
claim HepsKS:
SNo (eps_ K).
An
exact proof term for the current goal is
(real_SNo (eps_ K) HepsKR).
We prove the intermediate
claim HN0O:
N0 ∈ ω.
rewrite the current goal using
(add_nat_add_SNo K HKomega K HKomega) (from left to right).
An
exact proof term for the current goal is
(add_SNo_In_omega K HKomega K HKomega).
We prove the intermediate
claim HN0Nat:
nat_p N0.
An
exact proof term for the current goal is
(omega_nat_p N0 HN0O).
We prove the intermediate
claim HdenS:
SNo den.
An
exact proof term for the current goal is
(real_SNo den HdenR).
We prove the intermediate
claim HdenDef:
den = two_thirds.
We prove the intermediate
claim HdenLt1:
den < 1.
rewrite the current goal using HdenDef (from left to right).
Set den2 to be the term
mul_SNo den den.
We prove the intermediate
claim Hden2S:
SNo den2.
An
exact proof term for the current goal is
(SNo_mul_SNo den den HdenS HdenS).
We prove the intermediate
claim Hden2Lt_eps1:
den2 < eps_ 1.
rewrite the current goal using HdenDef (from left to right) at position 1.
rewrite the current goal using HdenDef (from left to right) at position 2.
Let m be given.
We prove the intermediate
claim HS:
State (ordsucc m) = StepState m (State m).
An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState m HmNat).
rewrite the current goal using HS (from left to right).
Set st to be the term State m.
Set c to be the term
(st 1) 1.
Set cNew to be the term
mul_SNo c den.
We prove the intermediate
claim HtEq:
((StepState m st) 1) 1 = cNew.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using Hinner (from left to right).
rewrite the current goal using HtEq (from left to right).
We prove the intermediate
claim HstEq:
st = State m.
We prove the intermediate
claim HcEq2:
c = ((State m) 1) 1.
rewrite the current goal using HstEq (from left to right).
Use reflexivity.
rewrite the current goal using HcEq2 (from left to right).
Use reflexivity.
We prove the intermediate
claim Hc_even_lt:
∀t : set, nat_p t → ((State (add_nat t t)) 1) 1 < eps_ t.
rewrite the current goal using
(add_nat_0R 0) (from left to right) at position 1.
rewrite the current goal using
eps_0_1 (from left to right).
Let t be given.
We prove the intermediate
claim HNnat:
nat_p N.
An
exact proof term for the current goal is
(add_nat_p t HtNat t HtNat).
rewrite the current goal using
(add_nat_SR t t HtNat) (from left to right).
Use reflexivity.
rewrite the current goal using Hidx (from left to right).
We prove the intermediate
claim HN0:
N ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega N HNnat).
We prove the intermediate
claim HcSN:
((State (ordsucc N)) 1) 1 = mul_SNo (((State N) 1) 1) den.
An exact proof term for the current goal is (Hc_step N HNnat).
An
exact proof term for the current goal is
(nat_ordsucc N HNnat).
rewrite the current goal using
(Hc_step (ordsucc N) HSNnat) (from left to right).
rewrite the current goal using HcSN (from left to right).
Use reflexivity.
rewrite the current goal using HcSSN (from left to right).
rewrite the current goal using
(mul_SNo_assoc (((State N) 1) 1) den den (real_SNo (((State N) 1) 1) (andEL (((State N) 1) 1 ∈ R) (0 < ((State N) 1) 1) (HInv_cpos N HN0))) HdenS HdenS) (from right to left).
We prove the intermediate
claim Hden2Def:
den2 = mul_SNo den den.
rewrite the current goal using Hden2Def (from right to left).
We prove the intermediate
claim HcNpos:
0 < ((State N) 1) 1.
An
exact proof term for the current goal is
(andER (((State N) 1) 1 ∈ R) (0 < ((State N) 1) 1) (HInv_cpos N HN0)).
We prove the intermediate
claim HcNS:
SNo (((State N) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State N) 1) 1) (andEL (((State N) 1) 1 ∈ R) (0 < ((State N) 1) 1) (HInv_cpos N HN0))).
rewrite the current goal using
(mul_SNo_com (((State N) 1) 1) den2 HcNS Hden2S) (from left to right).
We prove the intermediate
claim Heps1S0:
SNo (eps_ 1).
We prove the intermediate
claim Heps1pos:
0 < eps_ 1.
An
exact proof term for the current goal is
(pos_mul_SNo_Lt' den2 (eps_ 1) (((State N) 1) 1) Hden2S Heps1S0 HcNS HcNpos Hden2Lt_eps1).
We prove the intermediate
claim Heps_tR:
(eps_ t) ∈ R.
We prove the intermediate
claim Heps_tS:
SNo (eps_ t).
An
exact proof term for the current goal is
(real_SNo (eps_ t) Heps_tR).
An
exact proof term for the current goal is
(mul_SNo_com (eps_ 1) (((State N) 1) 1) Heps1S0 HcNS).
rewrite the current goal using HcomL (from left to right).
rewrite the current goal using HcomR (from left to right).
An
exact proof term for the current goal is
(pos_mul_SNo_Lt' (((State N) 1) 1) (eps_ t) (eps_ 1) HcNS Heps_tS Heps1S0 Heps1pos IH).
We prove the intermediate
claim Hordt:
ordinal t.
An
exact proof term for the current goal is
(nat_p_ordinal t HtNat).
Use reflexivity.
rewrite the current goal using HepsEq (from right to left).
An exact proof term for the current goal is HmulTra.
We prove the intermediate
claim HcN0:
((State N0) 1) 1 < eps_ K.
An exact proof term for the current goal is (Hc_even_lt K HKnat).
We prove the intermediate
claim HcN0R:
((State N0) 1) 1 ∈ R.
An
exact proof term for the current goal is
(andEL (((State N0) 1) 1 ∈ R) (0 < ((State N0) 1) 1) (HInv_cpos N0 HN0O)).
We prove the intermediate
claim HcN0S:
SNo (((State N0) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State N0) 1) 1) HcN0R).
We prove the intermediate
claim HcN0ltEta:
((State N0) 1) 1 < eta.
An
exact proof term for the current goal is
(SNoLt_tra (((State N0) 1) 1) (eps_ K) eta HcN0S HepsKS HetaS HcN0 HepsKltEtaS).
We use N0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN0O.
Let m and n be given.
Let x be given.
We prove the intermediate
claim HmNat:
nat_p m.
An
exact proof term for the current goal is
(omega_nat_p m HmO).
We prove the intermediate
claim HnNat:
nat_p n.
An
exact proof term for the current goal is
(omega_nat_p n HnO).
We prove the intermediate
claim Hexkm:
∃km : set, nat_p km ∧ m = add_nat km N0.
An
exact proof term for the current goal is
(nat_Subq_add_ex N0 HN0Nat m HmNat HNm).
Apply Hexkm to the current goal.
Let km be given.
Assume Hkm.
We prove the intermediate
claim HkmNat:
nat_p km.
We prove the intermediate
claim HmEq:
m = add_nat km N0.
rewrite the current goal using HmEq (from left to right).
We prove the intermediate
claim Hexkn:
∃kn : set, nat_p kn ∧ n = add_nat kn N0.
An
exact proof term for the current goal is
(nat_Subq_add_ex N0 HN0Nat n HnNat HNn).
Apply Hexkn to the current goal.
Let kn be given.
Assume Hkn.
We prove the intermediate
claim HknNat:
nat_p kn.
We prove the intermediate
claim HnEq:
n = add_nat kn N0.
rewrite the current goal using HnEq (from left to right).
We prove the intermediate
claim HmO2:
(add_nat km N0) ∈ ω.
We prove the intermediate
claim HnO2:
(add_nat kn N0) ∈ ω.
We prove the intermediate
claim HfnDef:
fn = graph ω (λk : set ⇒ (State k) 0).
An
exact proof term for the current goal is
(HInv_g_FS (add_nat km N0) HmO2).
An
exact proof term for the current goal is
(HInv_g_FS (add_nat kn N0) HnO2).
An exact proof term for the current goal is (Hm_on x HxX).
An exact proof term for the current goal is (Hn_on x HxX).
An exact proof term for the current goal is (HInv_g_FS N0 HN0O).
We prove the intermediate
claim HgN0_on:
function_on ((State N0) 0) X R.
We prove the intermediate
claim HgN0xR:
apply_fun ((State N0) 0) x ∈ R.
An exact proof term for the current goal is (HgN0_on x HxX).
We prove the intermediate
claim HgN0xS:
SNo (apply_fun ((State N0) 0) x).
An
exact proof term for the current goal is
(real_SNo (apply_fun ((State N0) 0) x) HgN0xR).
We prove the intermediate
claim HcN0S0:
SNo (((State N0) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State N0) 1) 1) HcN0R).
Let t be given.
Let x0 be given.
We prove the intermediate
claim HtO:
t ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega t HtNat).
We prove the intermediate
claim HtSuccO:
ordsucc t ∈ ω.
An
exact proof term for the current goal is
(omega_ordsucc t HtO).
Set r to be the term
((State t) 1) 0.
Set c to be the term
((State t) 1) 1.
Set cNew to be the term
mul_SNo c den.
We prove the intermediate
claim HS:
State (ordsucc t) = StepState t (State t).
An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState t HtNat).
rewrite the current goal using (Hc_step t HtNat) (from left to right) at position 1.
We prove the intermediate
claim HgSucc:
(State (ordsucc t)) 0 = gNew.
rewrite the current goal using HS (from left to right).
rewrite the current goal using HdefS (from left to right).
rewrite the current goal using Hproj0 (from left to right).
We prove the intermediate
claim HrEq:
r = ((State t) 1) 0.
We prove the intermediate
claim HcEq0:
c = ((State t) 1) 1.
rewrite the current goal using HrEq (from right to left).
rewrite the current goal using HcEq0 (from right to left).
rewrite the current goal using HcorrDef (from right to left).
rewrite the current goal using HgNewDef (from left to right).
Use reflexivity.
We prove the intermediate
claim HcEq:
c = ((State t) 1) 1.
We prove the intermediate
claim HcR:
c ∈ R.
rewrite the current goal using HcEq (from left to right).
An
exact proof term for the current goal is
(andEL (((State t) 1) 1 ∈ R) (0 < ((State t) 1) 1) (HInv_cpos t HtO)).
We prove the intermediate
claim HcS:
SNo c.
An
exact proof term for the current goal is
(real_SNo c HcR).
We prove the intermediate
claim HcPos:
0 < c.
rewrite the current goal using HcEq (from left to right).
An
exact proof term for the current goal is
(andER (((State t) 1) 1 ∈ R) (0 < ((State t) 1) 1) (HInv_cpos t HtO)).
We prove the intermediate
claim H0le_c:
0 ≤ c.
An
exact proof term for the current goal is
(SNoLtLe 0 c HcPos).
An exact proof term for the current goal is (HInv_r_contI t HtO).
An exact proof term for the current goal is (Hu_of_prop r Hr_contI).
We prove the intermediate
claim Hu_contI0:
continuous_map X Tx I0 T0 (u_of r).
We prove the intermediate
claim Hu_fun:
function_on (u_of r) X I0.
We prove the intermediate
claim HuxI0:
apply_fun (u_of r) x0 ∈ I0.
An exact proof term for the current goal is (Hu_fun x0 Hx0X).
We prove the intermediate
claim HuxR:
apply_fun (u_of r) x0 ∈ R.
We prove the intermediate
claim HuxS:
SNo (apply_fun (u_of r) x0).
rewrite the current goal using HcorrDef0 (from left to right).
rewrite the current goal using Hcomp (from left to right).
We prove the intermediate
claim HgxR:
apply_fun ((State t) 0) x0 ∈ R.
We prove the intermediate
claim HcorrR:
apply_fun corr x0 ∈ R.
rewrite the current goal using HcorrEq (from left to right).
rewrite the current goal using HgSucc (from left to right).
rewrite the current goal using HgNewEval (from left to right).
We prove the intermediate
claim Ha0S:
SNo (apply_fun ((State t) 0) x0).
We prove the intermediate
claim Hb0S:
SNo (apply_fun corr x0).
rewrite the current goal using Hassoc1 (from right to left) at position 1.
rewrite the current goal using Hcom1 (from left to right) at position 1.
rewrite the current goal using Hassoc2 (from left to right).
rewrite the current goal using Hinv (from left to right) at position 1.
rewrite the current goal using Hcancel (from left to right) at position 1.
rewrite the current goal using HcorrEq (from left to right).
We prove the intermediate
claim Hhi:
u ≤ one_third.
An
exact proof term for the current goal is
(abs_SNo_mul_eq u c HuxS HcS).
rewrite the current goal using Habsc (from left to right).
rewrite the current goal using
(nonneg_abs_SNo c H0le_c) (from left to right).
We prove the intermediate
claim HabsuS:
SNo (abs_SNo u).
An
exact proof term for the current goal is
(SNo_abs_SNo u HuxS).
We prove the intermediate
claim HdenEq:
den = two_thirds.
rewrite the current goal using HdenEq (from left to right) at position 1.
An
exact proof term for the current goal is
(mul_SNo_oneR c HcS).
rewrite the current goal using HsumEq (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using Hcan (from right to left) at position 1.
rewrite the current goal using Htmp (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using H13Eq (from right to left) at position 1.
An exact proof term for the current goal is Hc13Le.
Let k be given.
Let x0 be given.
Let x1 be given.
We prove the intermediate
claim Hadd0:
add_nat 0 N0 = N0.
An
exact proof term for the current goal is
(add_nat_0L N0 HN0Nat).
rewrite the current goal using Hadd0 (from left to right) at position 1.
rewrite the current goal using Hadd0 (from left to right) at position 1.
An exact proof term for the current goal is (HInv_g_FS N0 HN0O).
We prove the intermediate
claim HgN0_on:
function_on ((State N0) 0) X R.
We prove the intermediate
claim HgN0xR:
apply_fun ((State N0) 0) x1 ∈ R.
An exact proof term for the current goal is (HgN0_on x1 Hx1X).
We prove the intermediate
claim HgN0xS:
SNo (apply_fun ((State N0) 0) x1).
An
exact proof term for the current goal is
(real_SNo (apply_fun ((State N0) 0) x1) HgN0xR).
An
exact proof term for the current goal is
(SNoLe_ref 0).
Let kk be given.
Let x1 be given.
Set t to be the term
add_nat kk N0.
We prove the intermediate
claim HtNat:
nat_p t.
An
exact proof term for the current goal is
(add_nat_p kk HkkNat N0 HN0Nat).
We prove the intermediate
claim HtO:
t ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega t HtNat).
rewrite the current goal using
(add_nat_SL kk HkkNat N0 HN0Nat) (from left to right).
Use reflexivity.
rewrite the current goal using Hidx (from left to right) at position 1.
rewrite the current goal using Hidx (from left to right) at position 1.
We prove the intermediate
claim HtSuccNat:
nat_p (ordsucc t).
An
exact proof term for the current goal is
(nat_ordsucc t HtNat).
We prove the intermediate
claim HtSuccO:
ordsucc t ∈ ω.
An exact proof term for the current goal is (HInv_g_FS N0 HN0O).
We prove the intermediate
claim HgN0_on:
function_on ((State N0) 0) X R.
We prove the intermediate
claim HgN0xR:
apply_fun ((State N0) 0) x1 ∈ R.
An exact proof term for the current goal is (HgN0_on x1 Hx1X).
We prove the intermediate
claim HgN0xS:
SNo (apply_fun ((State N0) 0) x1).
An
exact proof term for the current goal is
(real_SNo (apply_fun ((State N0) 0) x1) HgN0xR).
An exact proof term for the current goal is (HInv_g_FS t HtO).
We prove the intermediate
claim Ht_on:
function_on ((State t) 0) X R.
We prove the intermediate
claim HtxR:
apply_fun ((State t) 0) x1 ∈ R.
An exact proof term for the current goal is (Ht_on x1 Hx1X).
We prove the intermediate
claim HtxS:
SNo (apply_fun ((State t) 0) x1).
An
exact proof term for the current goal is
(HInv_g_FS (ordsucc t) HtSuccO).
An exact proof term for the current goal is (HtSucc_on x1 Hx1X).
An exact proof term for the current goal is (Hstep_budget t HtNat x1 Hx1X).
An exact proof term for the current goal is (IH x1 Hx1X).
We prove the intermediate
claim HctR:
(((State t) 1) 1) ∈ R.
An
exact proof term for the current goal is
(andEL ((((State t) 1) 1 ∈ R)) (0 < (((State t) 1) 1)) (HInv_cpos t HtO)).
We prove the intermediate
claim HctS:
SNo (((State t) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State t) 1) 1) HctR).
We prove the intermediate
claim HctsR:
(((State (ordsucc t)) 1) 1) ∈ R.
We prove the intermediate
claim HctsS:
SNo (((State (ordsucc t)) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State (ordsucc t)) 1) 1) HctsR).
We prove the intermediate
claim Hc0S:
SNo (((State N0) 1) 1).
An exact proof term for the current goal is HcN0S0.
We prove the intermediate
claim HmctS:
SNo (minus_SNo (((State t) 1) 1)).
An
exact proof term for the current goal is
(SNo_minus_SNo (((State t) 1) 1) HctS).
We prove the intermediate
claim Ht2S:
SNo (add_SNo (((State N0) 1) 1) (((State t) 1) 1)).
An
exact proof term for the current goal is
(SNo_add_SNo (((State N0) 1) 1) (((State t) 1) 1) Hc0S HctS).
rewrite the current goal using Hinv (from left to right) at position 1.
Use reflexivity.
rewrite the current goal using HsumEq (from right to left) at position 1.
An exact proof term for the current goal is (Htail_strong_all k HkNat x0 Hx0X).
We prove the intermediate
claim HkN0Nat:
nat_p (add_nat k N0).
An
exact proof term for the current goal is
(add_nat_p k HkNat N0 HN0Nat).
We prove the intermediate
claim HkN0O:
(add_nat k N0) ∈ ω.
We prove the intermediate
claim HckR:
(((State (add_nat k N0)) 1) 1) ∈ R.
We prove the intermediate
claim HckS:
SNo (((State (add_nat k N0)) 1) 1).
An
exact proof term for the current goal is
(real_SNo (((State (add_nat k N0)) 1) 1) HckR).
We prove the intermediate
claim HckPos:
0 < (((State (add_nat k N0)) 1) 1).
We prove the intermediate
claim H0le_ck:
0 ≤ (((State (add_nat k N0)) 1) 1).
An
exact proof term for the current goal is
(SNoLtLe 0 (((State (add_nat k N0)) 1) 1) HckPos).
rewrite the current goal using
minus_SNo_0 (from left to right).
An
exact proof term for the current goal is
(SNoLe_ref 0).
We prove the intermediate
claim HmidLe:
add_SNo (((State N0) 1) 1) 0 ≤ ((State N0) 1) 1.
rewrite the current goal using
(add_SNo_0R (((State N0) 1) 1) HcN0S0) (from left to right).
An
exact proof term for the current goal is
(SNoLe_ref (((State N0) 1) 1)).
We prove the intermediate
claim HgN0xS:
SNo (apply_fun ((State N0) 0) x0).
An exact proof term for the current goal is (HInv_g_FS N0 HN0O).
We prove the intermediate
claim HgN0_on:
function_on ((State N0) 0) X R.
We prove the intermediate
claim HgN0xR:
apply_fun ((State N0) 0) x0 ∈ R.
An exact proof term for the current goal is (HgN0_on x0 Hx0X).
An
exact proof term for the current goal is
(real_SNo (apply_fun ((State N0) 0) x0) HgN0xR).
rewrite the current goal using HabSwap (from left to right).
We prove the intermediate
claim HetaSumEq:
add_SNo eta eta = eps0.
rewrite the current goal using
eps_0_1 (from left to right).
rewrite the current goal using
(mul_SNo_oneR eps0 Heps0S) (from left to right).
Use reflexivity.
rewrite the current goal using HetaSumEq (from right to left).
rewrite the current goal using HdefM (from left to right).
We prove the intermediate
claim HepsLt1:
Rlt eps 1.
An
exact proof term for the current goal is
(RltI eps 1 HepsR real_1 HepsLt1S).
An exact proof term for the current goal is (Huc_small eps HepsR HepsPos HepsLt1).
Apply HexN to the current goal.
Let N be given.
Assume HN.
We use N to witness the existential quantifier.
Apply andI to the current goal.
Let m and n be given.
Let x be given.
An exact proof term for the current goal is (HNprop m n HmO HnO HNm HNn x HxX).
We prove the intermediate
claim Hlt2:
Rlt (eps_ 1) eps.
rewrite the current goal using HepsEq1 (from left to right).
An
exact proof term for the current goal is
eps_1_lt1_R.
We prove the intermediate
claim H1LtEps:
Rlt 1 eps.
An
exact proof term for the current goal is
(RltI 1 eps real_1 HepsR H1LtEpsS).
We use
0 to
witness the existential quantifier.
Apply andI to the current goal.
Let m and n be given.
Let x be given.
We prove the intermediate
claim HfnDef:
fn = graph ω (λk : set ⇒ (State k) 0).
rewrite the current goal using
(apply_fun_of_graph_eq fn ω (λk : set ⇒ (State k) 0) m HfnDef HmO) (from left to right).
rewrite the current goal using
(apply_fun_of_graph_eq fn ω (λk : set ⇒ (State k) 0) n HfnDef HnO) (from left to right).
An exact proof term for the current goal is (HInv_g_FS m HmO).
An exact proof term for the current goal is (HInv_g_FS n HnO).
We prove the intermediate
claim Hm_on:
function_on ((State m) 0) X R.
We prove the intermediate
claim Hn_on:
function_on ((State n) 0) X R.
We prove the intermediate
claim HmxR:
apply_fun ((State m) 0) x ∈ R.
An exact proof term for the current goal is (Hm_on x HxX).
We prove the intermediate
claim HnxR:
apply_fun ((State n) 0) x ∈ R.
An exact proof term for the current goal is (Hn_on x HxX).
rewrite the current goal using HdefM (from left to right).
Apply Hexfn to the current goal.
Let fn be given.
We prove the intermediate
claim HfnRange:
∀n : set, n ∈ ω → ∀x : set, x ∈ X → apply_fun (apply_fun fn n) x ∈ I.
Apply HexgR to the current goal.
Let gR be given.
We use gR to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Let x be given.
An exact proof term for the current goal is Heq.
Apply FalseE to the current goal.
We prove the intermediate
claim HxX':
x ∈ X.
An exact proof term for the current goal is (HAsubX x HxA).
An exact proof term for the current goal is (HfnLimA x HxA).
We prove the intermediate
claim HgxR:
apply_fun gR x ∈ R.
An exact proof term for the current goal is (HgRfun x HxX').
We prove the intermediate
claim HfxR:
apply_fun f x ∈ R.
An exact proof term for the current goal is (Hf_R x HxA).
An exact proof term for the current goal is (Hneq Heq).
Let n be given.
An exact proof term for the current goal is (HfnRange n HnO x HxX').
Let x be given.
We prove the intermediate
claim HI_sub_R:
I ⊆ R.
We prove the intermediate
claim HseqxI:
∀n : set, n ∈ ω → apply_fun seqx n ∈ I.
Let n be given.
An exact proof term for the current goal is (HfnRange n HnO x HxX).