proposition: Lemma rtclosedP {g} : reflect (reflexive g /\ transitive g) (rtclosed g).
proof: Proof. apply: (iffP idP) => [/connect_eqP eqg|[grefl gtrans]]. split=> [x|y x z]; first by rewrite -eqg connect0. by rewrite -!eqg; apply: connect_trans. apply/sub_connectP => x y /connectP[p]. elim: p => //= [|z p IHp] in x *; first by move=> _ ->. by move=> /andP[gxz gzp] eqy; apply: gtrans gxz _; apply: IHp. Qed.
imports: mathcomp(all_ssreflect) extra