V : Type u_1
G : SimpleGraph V
u v : V
hconn : Connected G
hne : u ≠ v
h : dist G u v = 0
⊢ False
V : Type u_1
G : SimpleGraph V
u v : V
hconn : Connected G
hne : u ≠ v
⊢ dist G u v ≠ 0
intro h
no goals
V : Type u_1
G : SimpleGraph V
u v : V
hconn : Connected G
hne : u ≠ v
h : dist G u v = 0
⊢ False
exact False.elim (hne (hconn.dist_eq_zero_iff.mp h))