Let f, g and i be given.
Assume Hf: f ∈ real_sequences.
Assume Hg: g ∈ real_sequences.
Assume Hi: i ∈ ω.
Set A to be the term Romega_clipped_diffs f g.
Set l to be the term Romega_uniform_metric_value f g.
We prove the intermediate claim Hlub: R_lub A l.
An exact proof term for the current goal is (Romega_uniform_metric_value_is_lub f g Hf Hg).
Set P to be the term l ∈ R.
Set UB to be the term ∀a : set, a ∈ A → a ∈ R → Rle a l.
Set MIN to be the term ∀u : set, u ∈ R → (∀a : set, a ∈ A → a ∈ R → Rle a u) → Rle l u.
We prove the intermediate claim Hcore: P ∧ UB.
An exact proof term for the current goal is (andEL (P ∧ UB) MIN Hlub).
We prove the intermediate claim Hub: UB.
An exact proof term for the current goal is (andER P UB Hcore).
We prove the intermediate claim Hai: Romega_coord_clipped_diff f g i ∈ A.
An exact proof term for the current goal is (ReplI ω (λn : set ⇒ Romega_coord_clipped_diff f g n) i Hi).
We prove the intermediate claim HaiR: Romega_coord_clipped_diff f g i ∈ R.
An exact proof term for the current goal is (Romega_clipped_diffs_in_R f g Hf Hg (Romega_coord_clipped_diff f g i) Hai).
An exact proof term for the current goal is (Hub (Romega_coord_clipped_diff f g i) Hai HaiR).
∎