We will prove metric_on R R_bounded_metric.
We will prove ((((function_on R_bounded_metric (setprod R R) R ∧ (∀x y : set, x ∈ R → y ∈ R → apply_fun R_bounded_metric (x,y) = apply_fun R_bounded_metric (y,x))) ∧ (∀x : set, x ∈ R → apply_fun R_bounded_metric (x,x) = 0)) ∧ (∀x y : set, x ∈ R → y ∈ R → ¬ (Rlt (apply_fun R_bounded_metric (x,y)) 0) ∧ (apply_fun R_bounded_metric (x,y) = 0 → x = y))) ∧ (∀x y z : set, x ∈ R → y ∈ R → z ∈ R → ¬ (Rlt (add_SNo (apply_fun R_bounded_metric (x,y)) (apply_fun R_bounded_metric (y,z))) (apply_fun R_bounded_metric (x,z))))).
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 p be given.
Assume Hp: p ∈ setprod R R.
We will prove apply_fun R_bounded_metric p ∈ R.
We prove the intermediate claim Happ: apply_fun R_bounded_metric p = R_bounded_distance (p 0) (p 1).
An exact proof term for the current goal is (apply_fun_graph (setprod R R) (λq : set ⇒ R_bounded_distance (q 0) (q 1)) p Hp).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hp0: p 0 ∈ R.
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) p Hp).
We prove the intermediate claim Hp1: p 1 ∈ R.
An exact proof term for the current goal is (ap1_Sigma R (λ_ : set ⇒ R) p Hp).
An exact proof term for the current goal is (R_bounded_distance_in_R (p 0) (p 1) Hp0 Hp1).
Let x and y be given.
Assume Hx: x ∈ R.
Assume Hy: y ∈ R.
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x y Hx Hy).
We prove the intermediate claim Hyxprod: (y,x) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R y x Hy Hx).
rewrite the current goal using (apply_fun_graph (setprod R R) (λq : set ⇒ R_bounded_distance (q 0) (q 1)) (x,y) Hxyprod) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod R R) (λq : set ⇒ R_bounded_distance (q 0) (q 1)) (y,x) Hyxprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
rewrite the current goal using (tuple_2_0_eq y x) (from left to right).
rewrite the current goal using (tuple_2_1_eq y x) (from left to right).
An exact proof term for the current goal is (R_bounded_distance_sym x y Hx Hy).
Let x be given.
Assume Hx: x ∈ R.
We prove the intermediate claim Hxxprod: (x,x) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x x Hx Hx).
rewrite the current goal using (apply_fun_graph (setprod R R) (λq : set ⇒ R_bounded_distance (q 0) (q 1)) (x,x) Hxxprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x x) (from left to right).
rewrite the current goal using (tuple_2_1_eq x x) (from left to right).
An exact proof term for the current goal is (R_bounded_distance_self_zero x Hx).
Let x and y be given.
Assume Hx: x ∈ R.
Assume Hy: y ∈ R.
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x y Hx Hy).
We will prove ¬ (Rlt (apply_fun R_bounded_metric (x,y)) 0) ∧ (apply_fun R_bounded_metric (x,y) = 0 → x = y).
Apply andI to the current goal.
We will prove ¬ (Rlt (apply_fun R_bounded_metric (x,y)) 0).
rewrite the current goal using (apply_fun_graph (setprod R R) (λq : set ⇒ R_bounded_distance (q 0) (q 1)) (x,y) Hxyprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
We will prove ¬ (Rlt (R_bounded_distance x y) 0).
Assume Hlt: Rlt (R_bounded_distance x y) 0.
We prove the intermediate claim HdR: R_bounded_distance x y ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R x y Hx Hy).
We prove the intermediate claim HdS: SNo (R_bounded_distance x y).
An exact proof term for the current goal is (real_SNo (R_bounded_distance x y) HdR).
We prove the intermediate claim H0S: SNo 0.
An exact proof term for the current goal is SNo_0.
We prove the intermediate claim Hnonneg: 0 ≤ R_bounded_distance x y.
An exact proof term for the current goal is (R_bounded_distance_nonneg x y Hx Hy).
We prove the intermediate claim Hcase: 0 < (R_bounded_distance x y) ∨ 0 = (R_bounded_distance x y).
An exact proof term for the current goal is (SNoLeE 0 (R_bounded_distance x y) H0S HdS Hnonneg).
We prove the intermediate claim HltS: R_bounded_distance x y < 0.
An exact proof term for the current goal is (RltE_lt (R_bounded_distance x y) 0 Hlt).
Apply (Hcase False) to the current goal.
Assume H0ltd: 0 < (R_bounded_distance x y).
We prove the intermediate claim H00: 0 < 0.
An exact proof term for the current goal is (SNoLt_tra 0 (R_bounded_distance x y) 0 H0S HdS H0S H0ltd HltS).
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
Assume H0eq: 0 = (R_bounded_distance x y).
We prove the intermediate claim H00: 0 < 0.
rewrite the current goal using H0eq (from left to right) at position 1.
An exact proof term for the current goal is HltS.
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
Assume H0: apply_fun R_bounded_metric (x,y) = 0.
We prove the intermediate claim Happ: apply_fun R_bounded_metric (x,y) = R_bounded_distance x y.
rewrite the current goal using (apply_fun_graph (setprod R R) (λq : set ⇒ R_bounded_distance (q 0) (q 1)) (x,y) Hxyprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
Use reflexivity.
We prove the intermediate claim Hbd0: R_bounded_distance x y = 0.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is H0.
An exact proof term for the current goal is (R_bounded_distance_eq0 x y Hx Hy Hbd0).
Let x, y and z be given.
Assume Hx: x ∈ R.
Assume Hy: y ∈ R.
Assume Hz: z ∈ R.
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x y Hx Hy).
We prove the intermediate claim Hyzprod: (y,z) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R y z Hy Hz).
We prove the intermediate claim Hxzprod: (x,z) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x z Hx Hz).
rewrite the current goal using (apply_fun_graph (setprod R R) (λq : set ⇒ R_bounded_distance (q 0) (q 1)) (x,y) Hxyprod) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod R R) (λq : set ⇒ R_bounded_distance (q 0) (q 1)) (y,z) Hyzprod) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod R R) (λq : set ⇒ R_bounded_distance (q 0) (q 1)) (x,z) Hxzprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
rewrite the current goal using (tuple_2_0_eq y z) (from left to right).
rewrite the current goal using (tuple_2_1_eq y z) (from left to right).
rewrite the current goal using (tuple_2_0_eq x z) (from left to right).
rewrite the current goal using (tuple_2_1_eq x z) (from left to right).
We prove the intermediate claim Htri: R_bounded_distance x z ≤ add_SNo (R_bounded_distance x y) (R_bounded_distance y z).
An exact proof term for the current goal is (R_bounded_distance_triangle_Le x y z Hx Hy Hz).
We will prove ¬ (Rlt (add_SNo (R_bounded_distance x y) (R_bounded_distance y z)) (R_bounded_distance x z)).
Assume Hlt: Rlt (add_SNo (R_bounded_distance x y) (R_bounded_distance y z)) (R_bounded_distance x z).
We prove the intermediate claim HxzR: R_bounded_distance x z ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R x z Hx Hz).
We prove the intermediate claim HsumR: add_SNo (R_bounded_distance x y) (R_bounded_distance y z) ∈ R.
We prove the intermediate claim HxyR: R_bounded_distance x y ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R x y Hx Hy).
We prove the intermediate claim HyzR: R_bounded_distance y z ∈ R.
An exact proof term for the current goal is (R_bounded_distance_in_R y z Hy Hz).
An exact proof term for the current goal is (real_add_SNo (R_bounded_distance x y) HxyR (R_bounded_distance y z) HyzR).
We prove the intermediate claim HxzS: SNo (R_bounded_distance x z).
An exact proof term for the current goal is (real_SNo (R_bounded_distance x z) HxzR).
We prove the intermediate claim HsumS: SNo (add_SNo (R_bounded_distance x y) (R_bounded_distance y z)).
An exact proof term for the current goal is (real_SNo (add_SNo (R_bounded_distance x y) (R_bounded_distance y z)) HsumR).
We prove the intermediate claim Hcase: (R_bounded_distance x z) < (add_SNo (R_bounded_distance x y) (R_bounded_distance y z)) ∨ (R_bounded_distance x z) = (add_SNo (R_bounded_distance x y) (R_bounded_distance y z)).
An exact proof term for the current goal is (SNoLeE (R_bounded_distance x z) (add_SNo (R_bounded_distance x y) (R_bounded_distance y z)) HxzS HsumS Htri).
We prove the intermediate claim HltS: (add_SNo (R_bounded_distance x y) (R_bounded_distance y z)) < (R_bounded_distance x z).
An exact proof term for the current goal is (RltE_lt (add_SNo (R_bounded_distance x y) (R_bounded_distance y z)) (R_bounded_distance x z) Hlt).
Apply (Hcase False) to the current goal.
Assume Hxzlts: (R_bounded_distance x z) < (add_SNo (R_bounded_distance x y) (R_bounded_distance y z)).
We prove the intermediate claim Hbad: (R_bounded_distance x z) < (R_bounded_distance x z).
An exact proof term for the current goal is (SNoLt_tra (R_bounded_distance x z) (add_SNo (R_bounded_distance x y) (R_bounded_distance y z)) (R_bounded_distance x z) HxzS HsumS HxzS Hxzlts HltS).
An exact proof term for the current goal is ((SNoLt_irref (R_bounded_distance x z)) Hbad).
Assume Hxzeq: (R_bounded_distance x z) = (add_SNo (R_bounded_distance x y) (R_bounded_distance y z)).
We prove the intermediate claim Hbad: (R_bounded_distance x z) < (R_bounded_distance x z).
rewrite the current goal using Hxzeq (from left to right) at position 1.
An exact proof term for the current goal is HltS.
An exact proof term for the current goal is ((SNoLt_irref (R_bounded_distance x z)) Hbad).
∎