proposition: Lemma gdist_connect t1 t2 : connect r t1 t2 = (`d[t1,t2] < #|T|).
proof: Proof. apply/connectP/idP=> [[p /shortenP[p' Hp' Hu _ Ht]]|]. apply: leq_trans (_ : size p' < _). by apply: gdist_path_le. rewrite -[_.+1]/(size (t1 :: p')) cardE. apply: uniq_leq_size => // i. by rewrite mem_enum. rewrite -[#|_|](size_iota 0) -has_find. move => /hasP[n _ /connectnP [p [H1p H2p H3p]]]. by exists p. Qed.
imports: mathcomp(all_ssreflect)