Let f and g be given.
Assume Hf: f ∈ binary_sequences_Romega.
Assume Hg: g ∈ binary_sequences_Romega.
Assume Hneq: f ≠ g.
We prove the intermediate claim HfX: f ∈ real_sequences.
An exact proof term for the current goal is (SepE1 real_sequences (λf0 : set ⇒ ∀n : set, n ∈ ω → apply_fun f0 n ∈ {0,1}) f Hf).
We prove the intermediate claim HgX: g ∈ real_sequences.
An exact proof term for the current goal is (SepE1 real_sequences (λf0 : set ⇒ ∀n : set, n ∈ ω → apply_fun f0 n ∈ {0,1}) g Hg).
We prove the intermediate claim Hpair: (f,g) ∈ setprod real_sequences real_sequences.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma real_sequences real_sequences f g HfX HgX).
rewrite the current goal using (apply_fun_graph (setprod real_sequences real_sequences) (λp : set ⇒ Romega_uniform_metric_value (p 0) (p 1)) (f,g) Hpair) (from left to right).
We prove the intermediate claim H0: (f,g) 0 = f.
An exact proof term for the current goal is (tuple_2_0_eq f g).
We prove the intermediate claim H1: (f,g) 1 = g.
An exact proof term for the current goal is (tuple_2_1_eq f g).
rewrite the current goal using H0 (from left to right) at position 1.
rewrite the current goal using H1 (from left to right) at position 1.
Set A to be the term Romega_clipped_diffs f g.
Set P to be the term (λr : set ⇒ R_lub A r).
We prove the intermediate claim Hdef: Romega_uniform_metric_value f g = Eps_i P.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
We prove the intermediate claim Hlub1: R_lub A 1.
We will prove (1 ∈ R ∧ (∀a : set, a ∈ A → a ∈ R → Rle a 1)) ∧ (∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle 1 u).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is real_1.
Let a be given.
Assume Ha: a ∈ A.
Assume HaR: a ∈ R.
We will prove Rle a 1.
Apply (ReplE_impred ω (λn : set ⇒ Romega_coord_clipped_diff f g n) a Ha (Rle a 1)) to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Haeq: a = Romega_coord_clipped_diff f g n.
rewrite the current goal using Haeq (from left to right).
Apply (xm (Rlt (Romega_coord_abs_diff f g n) 1) (Rle (Romega_coord_clipped_diff f g n) 1)) to the current goal.
Assume Hlt: Rlt (Romega_coord_abs_diff f g n) 1.
We prove the intermediate claim Hdefc: Romega_coord_clipped_diff f g n = If_i (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1.
Use reflexivity.
rewrite the current goal using Hdefc (from left to right).
rewrite the current goal using (If_i_1 (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1 Hlt) (from left to right).
An exact proof term for the current goal is (Rlt_implies_Rle (Romega_coord_abs_diff f g n) 1 Hlt).
Assume Hnlt: ¬ (Rlt (Romega_coord_abs_diff f g n) 1).
We prove the intermediate claim Hdefc: Romega_coord_clipped_diff f g n = If_i (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1.
Use reflexivity.
rewrite the current goal using Hdefc (from left to right).
rewrite the current goal using (If_i_0 (Rlt (Romega_coord_abs_diff f g n) 1) (Romega_coord_abs_diff f g n) 1 Hnlt) (from left to right).
An exact proof term for the current goal is (Rle_refl 1 real_1).
Let u be given.
Assume HuR: u ∈ R.
Assume Hub: ∀a : set, a ∈ A → a ∈ R → Rle a u.
We will prove Rle 1 u.
We prove the intermediate claim Hexn: ∃n : set, n ∈ ω ∧ apply_fun f n ≠ apply_fun g n.
An exact proof term for the current goal is (real_sequences_neq_exists_coord f g HfX HgX Hneq).
Set n0 to be the term Eps_i (λn : set ⇒ n ∈ ω ∧ apply_fun f n ≠ apply_fun g n).
We prove the intermediate claim Hn0: n0 ∈ ω ∧ apply_fun f n0 ≠ apply_fun g n0.
An exact proof term for the current goal is (Eps_i_ex (λn : set ⇒ n ∈ ω ∧ apply_fun f n ≠ apply_fun g n) Hexn).
We prove the intermediate claim Hn0O: n0 ∈ ω.
An exact proof term for the current goal is (andEL (n0 ∈ ω) (apply_fun f n0 ≠ apply_fun g n0) Hn0).
We prove the intermediate claim Hn0neq: apply_fun f n0 ≠ apply_fun g n0.
An exact proof term for the current goal is (andER (n0 ∈ ω) (apply_fun f n0 ≠ apply_fun g n0) Hn0).
We prove the intermediate claim Hfvals: ∀n : set, n ∈ ω → apply_fun f n ∈ {0,1}.
An exact proof term for the current goal is (SepE2 real_sequences (λf0 : set ⇒ ∀n : set, n ∈ ω → apply_fun f0 n ∈ {0,1}) f Hf).
We prove the intermediate claim Hgvals: ∀n : set, n ∈ ω → apply_fun g n ∈ {0,1}.
An exact proof term for the current goal is (SepE2 real_sequences (λf0 : set ⇒ ∀n : set, n ∈ ω → apply_fun f0 n ∈ {0,1}) g Hg).
We prove the intermediate claim Hf0: apply_fun f n0 ∈ {0,1}.
An exact proof term for the current goal is (Hfvals n0 Hn0O).
We prove the intermediate claim Hg0: apply_fun g n0 ∈ {0,1}.
An exact proof term for the current goal is (Hgvals n0 Hn0O).
We prove the intermediate claim Hclip1: Romega_coord_clipped_diff f g n0 = 1.
Apply (UPairE (apply_fun f n0) 0 1 Hf0) to the current goal.
Assume Hfn0: apply_fun f n0 = 0.
Apply (UPairE (apply_fun g n0) 0 1 Hg0) to the current goal.
Assume Hgn0: apply_fun g n0 = 0.
We prove the intermediate claim Heq: apply_fun f n0 = apply_fun g n0.
rewrite the current goal using Hfn0 (from left to right).
rewrite the current goal using Hgn0 (from left to right).
Use reflexivity.
An exact proof term for the current goal is (FalseE (Hn0neq Heq) (Romega_coord_clipped_diff f g n0 = 1)).
Assume Hgn1: apply_fun g n0 = 1.
We prove the intermediate claim Habs: Romega_coord_abs_diff f g n0 = 1.
We prove the intermediate claim Hdefabs: Romega_coord_abs_diff f g n0 = abs_SNo (add_SNo (apply_fun f n0) (minus_SNo (apply_fun g n0))).
Use reflexivity.
rewrite the current goal using Hdefabs (from left to right).
rewrite the current goal using Hfn0 (from left to right).
rewrite the current goal using Hgn1 (from left to right).
rewrite the current goal using (add_SNo_0L (minus_SNo 1) (SNo_minus_SNo 1 SNo_1)) (from left to right).
rewrite the current goal using (abs_SNo_minus 1 SNo_1) (from left to right).
rewrite the current goal using (pos_abs_SNo 1 SNoLt_0_1) (from left to right).
Use reflexivity.
We prove the intermediate claim Hnlt: ¬ (Rlt (Romega_coord_abs_diff f g n0) 1).
rewrite the current goal using Habs (from left to right).
An exact proof term for the current goal is (not_Rlt_refl 1 real_1).
We prove the intermediate claim Hdefc: Romega_coord_clipped_diff f g n0 = If_i (Rlt (Romega_coord_abs_diff f g n0) 1) (Romega_coord_abs_diff f g n0) 1.
Use reflexivity.
rewrite the current goal using Hdefc (from left to right).
rewrite the current goal using (If_i_0 (Rlt (Romega_coord_abs_diff f g n0) 1) (Romega_coord_abs_diff f g n0) 1 Hnlt) (from left to right).
Use reflexivity.
Assume Hfn1: apply_fun f n0 = 1.
Apply (UPairE (apply_fun g n0) 0 1 Hg0) to the current goal.
Assume Hgn0: apply_fun g n0 = 0.
We prove the intermediate claim Habs: Romega_coord_abs_diff f g n0 = 1.
We prove the intermediate claim Hdefabs: Romega_coord_abs_diff f g n0 = abs_SNo (add_SNo (apply_fun f n0) (minus_SNo (apply_fun g n0))).
Use reflexivity.
rewrite the current goal using Hdefabs (from left to right).
rewrite the current goal using Hfn1 (from left to right).
rewrite the current goal using Hgn0 (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from left to right).
rewrite the current goal using (pos_abs_SNo 1 SNoLt_0_1) (from left to right).
Use reflexivity.
We prove the intermediate claim Hnlt: ¬ (Rlt (Romega_coord_abs_diff f g n0) 1).
rewrite the current goal using Habs (from left to right).
An exact proof term for the current goal is (not_Rlt_refl 1 real_1).
We prove the intermediate claim Hdefc: Romega_coord_clipped_diff f g n0 = If_i (Rlt (Romega_coord_abs_diff f g n0) 1) (Romega_coord_abs_diff f g n0) 1.
Use reflexivity.
rewrite the current goal using Hdefc (from left to right).
rewrite the current goal using (If_i_0 (Rlt (Romega_coord_abs_diff f g n0) 1) (Romega_coord_abs_diff f g n0) 1 Hnlt) (from left to right).
Use reflexivity.
Assume Hgn1: apply_fun g n0 = 1.
We prove the intermediate claim Heq: apply_fun f n0 = apply_fun g n0.
rewrite the current goal using Hfn1 (from left to right).
rewrite the current goal using Hgn1 (from left to right).
Use reflexivity.
An exact proof term for the current goal is (FalseE (Hn0neq Heq) (Romega_coord_clipped_diff f g n0 = 1)).
We prove the intermediate claim H1inA: 1 ∈ A.
We prove the intermediate claim Hin: Romega_coord_clipped_diff f g n0 ∈ A.
An exact proof term for the current goal is (ReplI ω (λn : set ⇒ Romega_coord_clipped_diff f g n) n0 Hn0O).
rewrite the current goal using Hclip1 (from right to left) at position 1.
An exact proof term for the current goal is Hin.
An exact proof term for the current goal is (Hub 1 H1inA real_1).
We prove the intermediate claim Hex: ∃r : set, P r.
We use 1 to witness the existential quantifier.
An exact proof term for the current goal is Hlub1.
We prove the intermediate claim HlubChosen: P (Eps_i P).
An exact proof term for the current goal is (Eps_i_ex P Hex).
An exact proof term for the current goal is (R_lub_unique A (Eps_i P) 1 HlubChosen Hlub1).
∎