Let X be given.
Set g to be the term λp : set ⇒ if (p 0 = p 1) then 0 else 1 of type set → set.
Set d to be the term graph (setprod X X) g of type set.
We use d to witness the existential quantifier.
We will prove metric_on X d.
We will prove ((((function_on d (setprod X X) R ∧ (∀x y : set, x ∈ X → y ∈ X → apply_fun d (x,y) = apply_fun d (y,x))) ∧ (∀x : set, x ∈ X → apply_fun d (x,x) = 0)) ∧ (∀x y : set, x ∈ X → y ∈ X → ¬ (Rlt (apply_fun d (x,y)) 0) ∧ (apply_fun d (x,y) = 0 → x = y))) ∧ (∀x y z : set, x ∈ X → y ∈ X → z ∈ X → ¬ (Rlt (add_SNo (apply_fun d (x,y)) (apply_fun d (y,z))) (apply_fun d (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.
We will prove function_on d (setprod X X) R.
Let p be given.
Assume Hp: p ∈ setprod X X.
We will prove apply_fun d p ∈ R.
rewrite the current goal using (apply_fun_graph (setprod X X) g p Hp) (from left to right).
Apply (xm (p 0 = p 1) ((if (p 0 = p 1) then 0 else 1) ∈ R)) to the current goal.
Assume H01: p 0 = p 1.
rewrite the current goal using (If_i_1 (p 0 = p 1) 0 1 H01) (from left to right).
An exact proof term for the current goal is real_0.
Assume H01n: ¬ (p 0 = p 1).
rewrite the current goal using (If_i_0 (p 0 = p 1) 0 1 H01n) (from left to right).
An exact proof term for the current goal is real_1.
Let x and y be given.
Assume Hx: x ∈ X.
Assume Hy: y ∈ X.
We will prove apply_fun d (x,y) = apply_fun d (y,x).
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y Hx Hy).
We prove the intermediate claim Hyxprod: (y,x) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X y x Hy Hx).
rewrite the current goal using (apply_fun_graph (setprod X X) g (x,y) Hxyprod) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) g (y,x) Hyxprod) (from left to right).
Apply (xm (x = y) ((if (x,y) 0 = (x,y) 1 then 0 else 1) = (if (y,x) 0 = (y,x) 1 then 0 else 1))) to the current goal.
Assume Hxy: x = y.
We prove the intermediate claim H01: (x,y) 0 = (x,y) 1.
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).
An exact proof term for the current goal is Hxy.
We prove the intermediate claim H10: (y,x) 0 = (y,x) 1.
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).
Use symmetry.
An exact proof term for the current goal is Hxy.
rewrite the current goal using (If_i_1 ((x,y) 0 = (x,y) 1) 0 1 H01) (from left to right).
rewrite the current goal using (If_i_1 ((y,x) 0 = (y,x) 1) 0 1 H10) (from left to right).
Use reflexivity.
Assume HxyN: ¬ (x = y).
We prove the intermediate claim H01n: ¬ ((x,y) 0 = (x,y) 1).
Assume H01.
Apply HxyN to the current goal.
We will prove x = y.
We prove the intermediate claim H0: (x,y) 0 = x.
An exact proof term for the current goal is (tuple_2_0_eq x y).
We prove the intermediate claim H1: (x,y) 1 = y.
An exact proof term for the current goal is (tuple_2_1_eq x y).
rewrite the current goal using H0 (from right to left) at position 1.
rewrite the current goal using H1 (from right to left) at position 2.
An exact proof term for the current goal is H01.
We prove the intermediate claim H10n: ¬ ((y,x) 0 = (y,x) 1).
Assume H10.
Apply HxyN to the current goal.
We will prove x = y.
We prove the intermediate claim Hy0: (y,x) 0 = y.
An exact proof term for the current goal is (tuple_2_0_eq y x).
We prove the intermediate claim Hx1: (y,x) 1 = x.
An exact proof term for the current goal is (tuple_2_1_eq y x).
rewrite the current goal using Hx1 (from right to left) at position 1.
rewrite the current goal using Hy0 (from right to left) at position 2.
Use symmetry.
An exact proof term for the current goal is H10.
rewrite the current goal using (If_i_0 ((x,y) 0 = (x,y) 1) 0 1 H01n) (from left to right).
rewrite the current goal using (If_i_0 ((y,x) 0 = (y,x) 1) 0 1 H10n) (from left to right).
Use reflexivity.
Let x be given.
Assume Hx: x ∈ X.
We will prove apply_fun d (x,x) = 0.
We prove the intermediate claim Hxxprod: (x,x) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x x Hx Hx).
rewrite the current goal using (apply_fun_graph (setprod X X) g (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).
We prove the intermediate claim Hrefl: x = x.
Use reflexivity.
rewrite the current goal using (If_i_1 (x = x) 0 1 Hrefl) (from left to right).
Use reflexivity.
Let x and y be given.
Assume Hx: x ∈ X.
Assume Hy: y ∈ X.
We will prove ¬ (Rlt (apply_fun d (x,y)) 0) ∧ (apply_fun d (x,y) = 0 → x = y).
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y Hx Hy).
rewrite the current goal using (apply_fun_graph (setprod X X) g (x,y) Hxyprod) (from left to right).
Apply (xm (x = y) (¬ (Rlt (if (x,y) 0 = (x,y) 1 then 0 else 1) 0) ∧ ((if (x,y) 0 = (x,y) 1 then 0 else 1) = 0 → x = y))) to the current goal.
Assume Hxy: x = y.
We prove the intermediate claim H01: (x,y) 0 = (x,y) 1.
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).
An exact proof term for the current goal is Hxy.
rewrite the current goal using (If_i_1 ((x,y) 0 = (x,y) 1) 0 1 H01) (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is (not_Rlt_refl 0 real_0).
Assume _.
An exact proof term for the current goal is Hxy.
Assume HxyN: ¬ (x = y).
We prove the intermediate claim H01n: ¬ ((x,y) 0 = (x,y) 1).
Assume H01.
Apply HxyN to the current goal.
We will prove x = y.
We prove the intermediate claim H0: (x,y) 0 = x.
An exact proof term for the current goal is (tuple_2_0_eq x y).
We prove the intermediate claim H1: (x,y) 1 = y.
An exact proof term for the current goal is (tuple_2_1_eq x y).
rewrite the current goal using H0 (from right to left) at position 1.
rewrite the current goal using H1 (from right to left) at position 2.
An exact proof term for the current goal is H01.
rewrite the current goal using (If_i_0 ((x,y) 0 = (x,y) 1) 0 1 H01n) (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is (not_Rlt_sym 0 1 Rlt_0_1).
Assume H10: 1 = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (neq_1_0 H10).
Let x, y and z be given.
Assume Hx: x ∈ X.
Assume Hy: y ∈ X.
Assume Hz: z ∈ X.
We will prove ¬ (Rlt (add_SNo (apply_fun d (x,y)) (apply_fun d (y,z))) (apply_fun d (x,z))).
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x y Hx Hy).
We prove the intermediate claim Hyzprod: (y,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X y z Hy Hz).
We prove the intermediate claim Hxzprod: (x,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x z Hx Hz).
rewrite the current goal using (apply_fun_graph (setprod X X) g (x,y) Hxyprod) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) g (y,z) Hyzprod) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod X X) g (x,z) Hxzprod) (from left to right).
Apply (xm (x = y) (¬ (Rlt (add_SNo (if (x,y) 0 = (x,y) 1 then 0 else 1) (if (y,z) 0 = (y,z) 1 then 0 else 1)) (if (x,z) 0 = (x,z) 1 then 0 else 1)))) to the current goal.
Assume Hxy: x = y.
We prove the intermediate claim Hxy01: (x,y) 0 = (x,y) 1.
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).
An exact proof term for the current goal is Hxy.
rewrite the current goal using (If_i_1 ((x,y) 0 = (x,y) 1) 0 1 Hxy01) (from left to right).
Apply (xm (y = z) (¬ (Rlt (add_SNo 0 (if (y,z) 0 = (y,z) 1 then 0 else 1)) (if (x,z) 0 = (x,z) 1 then 0 else 1)))) to the current goal.
Assume Hyz: y = z.
We prove the intermediate claim Hyz01: (y,z) 0 = (y,z) 1.
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).
An exact proof term for the current goal is Hyz.
We prove the intermediate claim Hxz: x = z.
rewrite the current goal using Hxy (from left to right).
An exact proof term for the current goal is Hyz.
We prove the intermediate claim Hxz01: (x,z) 0 = (x,z) 1.
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).
An exact proof term for the current goal is Hxz.
rewrite the current goal using (If_i_1 ((y,z) 0 = (y,z) 1) 0 1 Hyz01) (from left to right).
rewrite the current goal using (If_i_1 ((x,z) 0 = (x,z) 1) 0 1 Hxz01) (from left to right).
rewrite the current goal using (add_SNo_0L 0 SNo_0) (from left to right).
An exact proof term for the current goal is (not_Rlt_refl 0 real_0).
Assume HyzN: ¬ (y = z).
We prove the intermediate claim Hyz01n: ¬ ((y,z) 0 = (y,z) 1).
Assume H01.
Apply HyzN to the current goal.
We will prove y = z.
We prove the intermediate claim H0: (y,z) 0 = y.
An exact proof term for the current goal is (tuple_2_0_eq y z).
We prove the intermediate claim H1: (y,z) 1 = z.
An exact proof term for the current goal is (tuple_2_1_eq y z).
rewrite the current goal using H0 (from right to left) at position 1.
rewrite the current goal using H1 (from right to left) at position 2.
An exact proof term for the current goal is H01.
We prove the intermediate claim Hxz01n: ¬ ((x,z) 0 = (x,z) 1).
Assume H01.
Apply HyzN to the current goal.
We will prove y = z.
rewrite the current goal using Hxy (from right to left).
We prove the intermediate claim H0: (x,z) 0 = x.
An exact proof term for the current goal is (tuple_2_0_eq x z).
We prove the intermediate claim H1: (x,z) 1 = z.
An exact proof term for the current goal is (tuple_2_1_eq x z).
rewrite the current goal using H0 (from right to left) at position 1.
rewrite the current goal using H1 (from right to left) at position 2.
An exact proof term for the current goal is H01.
rewrite the current goal using (If_i_0 ((y,z) 0 = (y,z) 1) 0 1 Hyz01n) (from left to right).
rewrite the current goal using (If_i_0 ((x,z) 0 = (x,z) 1) 0 1 Hxz01n) (from left to right).
rewrite the current goal using (add_SNo_0L 1 SNo_1) (from left to right).
An exact proof term for the current goal is (not_Rlt_refl 1 real_1).
Assume HxyN: ¬ (x = y).
We prove the intermediate claim Hxy01n: ¬ ((x,y) 0 = (x,y) 1).
Assume H01.
Apply HxyN to the current goal.
We will prove x = y.
We prove the intermediate claim H0: (x,y) 0 = x.
An exact proof term for the current goal is (tuple_2_0_eq x y).
We prove the intermediate claim H1: (x,y) 1 = y.
An exact proof term for the current goal is (tuple_2_1_eq x y).
rewrite the current goal using H0 (from right to left) at position 1.
rewrite the current goal using H1 (from right to left) at position 2.
An exact proof term for the current goal is H01.
rewrite the current goal using (If_i_0 ((x,y) 0 = (x,y) 1) 0 1 Hxy01n) (from left to right).
Apply (xm (y = z) (¬ (Rlt (add_SNo 1 (if (y,z) 0 = (y,z) 1 then 0 else 1)) (if (x,z) 0 = (x,z) 1 then 0 else 1)))) to the current goal.
Assume Hyz: y = z.
We prove the intermediate claim Hyz01: (y,z) 0 = (y,z) 1.
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).
An exact proof term for the current goal is Hyz.
We prove the intermediate claim Hxz01n: ¬ ((x,z) 0 = (x,z) 1).
Assume H01.
Apply HxyN to the current goal.
We will prove x = y.
rewrite the current goal using Hyz (from left to right).
We prove the intermediate claim H0: (x,z) 0 = x.
An exact proof term for the current goal is (tuple_2_0_eq x z).
We prove the intermediate claim H1: (x,z) 1 = z.
An exact proof term for the current goal is (tuple_2_1_eq x z).
rewrite the current goal using H0 (from right to left) at position 1.
rewrite the current goal using H1 (from right to left) at position 2.
An exact proof term for the current goal is H01.
rewrite the current goal using (If_i_1 ((y,z) 0 = (y,z) 1) 0 1 Hyz01) (from left to right).
rewrite the current goal using (If_i_0 ((x,z) 0 = (x,z) 1) 0 1 Hxz01n) (from left to right).
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from left to right).
An exact proof term for the current goal is (not_Rlt_refl 1 real_1).
Assume HyzN: ¬ (y = z).
We prove the intermediate claim Hyz01n: ¬ ((y,z) 0 = (y,z) 1).
Assume H01.
Apply HyzN to the current goal.
We will prove y = z.
We prove the intermediate claim H0: (y,z) 0 = y.
An exact proof term for the current goal is (tuple_2_0_eq y z).
We prove the intermediate claim H1: (y,z) 1 = z.
An exact proof term for the current goal is (tuple_2_1_eq y z).
rewrite the current goal using H0 (from right to left) at position 1.
rewrite the current goal using H1 (from right to left) at position 2.
An exact proof term for the current goal is H01.
rewrite the current goal using (If_i_0 ((y,z) 0 = (y,z) 1) 0 1 Hyz01n) (from left to right).
Apply (xm (x = z) (¬ (Rlt (add_SNo 1 1) (if (x,z) 0 = (x,z) 1 then 0 else 1)))) to the current goal.
Assume Hxz: x = z.
We prove the intermediate claim Hxz01: (x,z) 0 = (x,z) 1.
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).
An exact proof term for the current goal is Hxz.
rewrite the current goal using (If_i_1 ((x,z) 0 = (x,z) 1) 0 1 Hxz01) (from left to right).
rewrite the current goal using add_SNo_1_1_2 (from left to right).
We prove the intermediate claim H0lt2: Rlt 0 2.
An exact proof term for the current goal is (RltI 0 2 real_0 real_2 SNoLt_0_2).
An exact proof term for the current goal is (not_Rlt_sym 0 2 H0lt2).
Assume HxzN: ¬ (x = z).
We prove the intermediate claim Hxz01n: ¬ ((x,z) 0 = (x,z) 1).
Assume H01.
Apply HxzN to the current goal.
We will prove x = z.
We prove the intermediate claim H0: (x,z) 0 = x.
An exact proof term for the current goal is (tuple_2_0_eq x z).
We prove the intermediate claim H1: (x,z) 1 = z.
An exact proof term for the current goal is (tuple_2_1_eq x z).
rewrite the current goal using H0 (from right to left) at position 1.
rewrite the current goal using H1 (from right to left) at position 2.
An exact proof term for the current goal is H01.
rewrite the current goal using (If_i_0 ((x,z) 0 = (x,z) 1) 0 1 Hxz01n) (from left to right).
rewrite the current goal using add_SNo_1_1_2 (from left to right).
We prove the intermediate claim H12: Rlt 1 2.
An exact proof term for the current goal is (RltI 1 2 real_1 real_2 SNoLt_1_2).
An exact proof term for the current goal is (not_Rlt_sym 1 2 H12).
∎