proposition: Lemma gdist_neighboor t1 t2 t3 : r t1 t2 -> r t2 t1 -> [|| `d[t2, t3] == `d[t1, t3].-1, `d[t2, t3] == `d[t1, t3] | `d[t2, t3] == `d[t1, t3].+1].
proof: Proof. move=> t1Rt2 t2Rt1. have : `d[t1, t3] - `d[t1, t2] <= `d[t2, t3] <= `d[t2, t1] + `d[t1, t3]. by rewrite leq_subLR !gdist_triangular. rewrite (gdist1 t1Rt2) (gdist1 t2Rt1). (do 2 case: eqP) => //= E1 E2; rewrite ?subn0. - by rewrite -eqn_leq => /eqP->; rewrite eqxx orbT. - case/andP=> E3. rewrite leq_eqVlt => /orP[/eqP->|]. by rewrite eqxx !orbT. rewrite ltnS => E4. by rewrite [`d[_, _] == `d[_, _]]eqn_leq E3 E4 orbT. - case/andP=> E3. rewrite leq_eqVlt => /orP[/eqP->|]. by rewrite eqxx !orbT. case: (`d[t1, t3]) E3 => //= d. rewrite subSS subn0 ltnS => E3 E4. by rewrite [_ == d]eqn_leq E3 E4. case/andP=> E3. rewrite leq_eqVlt => /orP[/eqP->|]. by rewrite eqxx !orbT. rewrite ltnS leq_eqVlt => /orP[/eqP->|]. by rewrite eqxx !orbT. case: (`d[t1, t3]) E3 => //= d. rewrite subSS subn0 ltnS => E3 E4. by rewrite [_ == d]eqn_leq E3 E4. Qed.
imports: mathcomp(all_ssreflect)