proposition: Lemma gdist_eq0 t1 t2 : (`d[t1, t2] == 0) = (t1 == t2).
proof: Proof. have tG : #|T| > 0 by rewrite (cardD1 t1). rewrite /gdist. case: #|_| tG => // n _. rewrite (iotaD _ 1) /= inE [t2 == _]eq_sym. by case: (t1 =P t2). Qed.
imports: mathcomp(all_ssreflect)