proposition: Lemma gdist1 t1 t2 : r t1 t2 -> `d[t1, t2] = (t1 != t2).
proof: Proof. move=> Hr; apply/eqP. case: (t1 =P t2) => [<-|/eqP HE]; first by rewrite gdist_eq0. rewrite eqn_leq -{1}[nat_of_bool _]/(size [::t2]) gdist_path_le /= ?andbT //. by case: gdist (gdist_eq0 t1 t2); rewrite (negPf HE) . Qed.
imports: mathcomp(all_ssreflect)