proposition: Lemma connect_sub e e' : subrel e (connect e') -> subrel (connect e) (connect e').
proof: Proof. move=> e'e x _ /connectP[p e_p ->]; elim: p x e_p => //= y p IHp x /andP[exy]. by move/IHp; apply: connect_trans; apply: e'e. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)