Let X be given.
We will prove metric_on X (discrete_metric X).
We will prove function_on (discrete_metric X) (setprod X X) R ∧ (∀x y : set, x ∈ X → y ∈ X → apply_fun (discrete_metric X) (x,y) = apply_fun (discrete_metric X) (y,x)) ∧ (∀x : set, x ∈ X → apply_fun (discrete_metric X) (x,x) = 0) ∧ (∀x y : set, x ∈ X → y ∈ X → ¬ (Rlt (apply_fun (discrete_metric X) (x,y)) 0) ∧ (apply_fun (discrete_metric X) (x,y) = 0 → x = y)) ∧ (∀x y z : set, x ∈ X → y ∈ X → z ∈ X → ¬ (Rlt (add_SNo (apply_fun (discrete_metric X) (x,y)) (apply_fun (discrete_metric X) (y,z))) (apply_fun (discrete_metric X) (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 X X.
We will prove apply_fun (discrete_metric X) p ∈ R.
Set x to be the term p 0.
Set y to be the term p 1.
We prove the intermediate claim Hx: x ∈ X.
An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ X) p Hp).
We prove the intermediate claim Hy: y ∈ X.
An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ X) p Hp).
We prove the intermediate claim Hpeta: p = (x,y).
An exact proof term for the current goal is (setprod_eta X X p Hp).
rewrite the current goal using Hpeta (from left to right).
rewrite the current goal using (discrete_metric_apply X x y Hx Hy) (from left to right).
Apply xm (x = y) to the current goal.
Assume Heq: x = y.
rewrite the current goal using (If_i_1 (x = y) 0 1 Heq) (from left to right).
An exact proof term for the current goal is real_0.
Assume Hneq: ¬ (x = y).
rewrite the current goal using (If_i_0 (x = y) 0 1 Hneq) (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.
rewrite the current goal using (discrete_metric_apply X x y Hx Hy) (from left to right).
rewrite the current goal using (discrete_metric_apply X y x Hy Hx) (from left to right).
Apply xm (x = y) to the current goal.
Assume Heq: x = y.
rewrite the current goal using (If_i_1 (x = y) 0 1 Heq) (from left to right).
rewrite the current goal using (If_i_1 (y = x) 0 1) (from left to right).
Use reflexivity.
rewrite the current goal using Heq (from left to right).
Use reflexivity.
Assume Hneq: ¬ (x = y).
rewrite the current goal using (If_i_0 (x = y) 0 1 Hneq) (from left to right).
We prove the intermediate claim Hnyx: ¬ (y = x).
Assume Hyx: y = x.
Apply Hneq to the current goal.
rewrite the current goal using Hyx (from right to left).
Use reflexivity.
rewrite the current goal using (If_i_0 (y = x) 0 1 Hnyx) (from left to right).
Use reflexivity.
Let x be given.
Assume Hx: x ∈ X.
rewrite the current goal using (discrete_metric_apply X x x Hx Hx) (from left to right).
rewrite the current goal using (If_i_1 (x = x) 0 1) (from left to right).
Use reflexivity.
Use reflexivity.
Let x and y be given.
Assume Hx: x ∈ X.
Assume Hy: y ∈ X.
We will prove ¬ (Rlt (apply_fun (discrete_metric X) (x,y)) 0) ∧ (apply_fun (discrete_metric X) (x,y) = 0 → x = y).
Apply andI to the current goal.
rewrite the current goal using (discrete_metric_apply X x y Hx Hy) (from left to right).
Apply xm (x = y) to the current goal.
Assume Heq: x = y.
rewrite the current goal using (If_i_1 (x = y) 0 1 Heq) (from left to right).
An exact proof term for the current goal is (not_Rlt_refl 0 real_0).
Assume Hneq: ¬ (x = y).
rewrite the current goal using (If_i_0 (x = y) 0 1 Hneq) (from left to right).
An exact proof term for the current goal is (not_Rlt_sym 0 1 Rlt_0_1).
Assume Hd0: apply_fun (discrete_metric X) (x,y) = 0.
We prove the intermediate claim Hd0': If_i (x = y) 0 1 = 0.
rewrite the current goal using (discrete_metric_apply X x y Hx Hy) (from right to left).
An exact proof term for the current goal is Hd0.
Apply xm (x = y) to the current goal.
Assume Heq: x = y.
An exact proof term for the current goal is Heq.
Assume Hneq: ¬ (x = y).
We prove the intermediate claim Hval: If_i (x = y) 0 1 = 1.
An exact proof term for the current goal is (If_i_0 (x = y) 0 1 Hneq).
Apply FalseE to the current goal.
We prove the intermediate claim H10: 1 = 0.
rewrite the current goal using Hval (from right to left) at position 1.
An exact proof term for the current goal is Hd0'.
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.
rewrite the current goal using (discrete_metric_apply X x y Hx Hy) (from left to right).
rewrite the current goal using (discrete_metric_apply X y z Hy Hz) (from left to right).
rewrite the current goal using (discrete_metric_apply X x z Hx Hz) (from left to right).
Apply xm (x = z) to the current goal.
Assume Hxz: x = z.
rewrite the current goal using (If_i_1 (x = z) 0 1 Hxz) (from left to right).
Apply xm (x = y) to the current goal.
Assume Hxy: x = y.
rewrite the current goal using (If_i_1 (x = y) 0 1 Hxy) (from left to right).
Apply xm (y = z) to the current goal.
Assume Hyz: y = z.
rewrite the current goal using (If_i_1 (y = z) 0 1 Hyz) (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 Hnyz: ¬ (y = z).
rewrite the current goal using (If_i_0 (y = z) 0 1 Hnyz) (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_sym 0 1 Rlt_0_1).
Assume Hnxy: ¬ (x = y).
rewrite the current goal using (If_i_0 (x = y) 0 1 Hnxy) (from left to right).
Apply xm (y = z) to the current goal.
Assume Hyz: y = z.
rewrite the current goal using (If_i_1 (y = z) 0 1 Hyz) (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_sym 0 1 Rlt_0_1).
Assume Hnyz: ¬ (y = z).
rewrite the current goal using (If_i_0 (y = z) 0 1 Hnyz) (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 Hnxz: ¬ (x = z).
rewrite the current goal using (If_i_0 (x = z) 0 1 Hnxz) (from left to right).
Apply xm (x = y) to the current goal.
Assume Hxy: x = y.
rewrite the current goal using (If_i_1 (x = y) 0 1 Hxy) (from left to right).
Apply xm (y = z) to the current goal.
Assume Hyz: y = z.
rewrite the current goal using (If_i_1 (y = z) 0 1 Hyz) (from left to right).
rewrite the current goal using (add_SNo_0L 0 SNo_0) (from left to right).
Apply FalseE to the current goal.
Apply Hnxz to the current goal.
rewrite the current goal using Hxy (from left to right).
An exact proof term for the current goal is Hyz.
Assume Hnyz: ¬ (y = z).
rewrite the current goal using (If_i_0 (y = z) 0 1 Hnyz) (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 Hnxy: ¬ (x = y).
rewrite the current goal using (If_i_0 (x = y) 0 1 Hnxy) (from left to right).
Apply xm (y = z) to the current goal.
Assume Hyz: y = z.
rewrite the current goal using (If_i_1 (y = z) 0 1 Hyz) (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 Hnyz: ¬ (y = z).
rewrite the current goal using (If_i_0 (y = z) 0 1 Hnyz) (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).
∎