case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ 0 ≤ dist x x

case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ 0 ≤ dist x y
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ 0 ≤ dist x y
rcases eq_or_ne x y with (rfl | h)
no goals
case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ 0 ≤ dist x x
simp [dist]
no goals
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ 0 ≤ dist x y
simp [dist, h, zero_le_two]