proposition: Lemma sdecomp_subrel (V : finType) (e1 e2 : rel V) (T:forest) (D : T -> {set V}) (e1_sym : symmetric e1) (e1_irrefl : irreflexive e1) (e2_sym : symmetric e2) (e2_irrefl : irreflexive e2): subrel e2 e1 -> sdecomp T (SGraph e1_sym e1_irrefl) D -> sdecomp T (SGraph e2_sym e2_irrefl) D.
proof: Proof. move => E [D1 D2 D3]. split => //=. move => x y /= xy. apply: D2 => /=. exact: E xy. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)