proposition: Lemma gdist_nconnect t1 t2 : ~~ connect r t1 t2 -> `d[t1,t2] = #|T|.
proof: Proof. move=> H; apply/eqP. have := gdist_card_le t1 t2. by rewrite leq_eqVlt -gdist_connect (negPf H) orbF. Qed.
imports: mathcomp(all_ssreflect)