proposition: Lemma rstclosedP {g} : reflect (equivalence_rel g) (rstclosed g).
proof: Proof. apply: (iffP idP) => [/symconnect_eqP gP|/equiv_relP[{}g->]]. by rewrite -(eq_equivalence_rel gP). by apply/sub_symconnectP; split=> // x y /andP[]; rewrite !(connect_eqP _). Qed.
imports: mathcomp(all_ssreflect) extra