proposition: Lemma sub_in_connect (T : finType) (e e' : rel T) (x : T) : (forall y, connect e x y -> e y =1 e' y) -> forall y, connect e x y -> connect e' x y.
proof: Proof. move => H y /connectP [p]. elim/last_ind : p y => [y _ -> //|p z IHp y]. rewrite rcons_path last_rcons => /andP[pth_p ez -> {y}]. rewrite H in ez; last by apply/connectP; exists p. apply: connect_trans (connect1 ez). exact: IHp. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)