proposition: Lemma gpathP t1 t2 p : reflect ([/\ path r t1 p, last t1 p = t2 & `d[t1, t2] = size p]) (gpath t1 t2 p).
proof: Proof. apply: (iffP and3P) => [[t1Pp /eqP t1pLt2 /eqP t1t2D]| [t1Pp t1pLt2 t1t2D]]; first by split. by split => //; apply/eqP. Qed.
imports: mathcomp(all_ssreflect)