proposition: Lemma smerge2Ecase (G : sgraph) (x y : G) (G' := smerge2 G x y) (P : G' -> G' -> Prop) : ~~ x -- y -> (forall u v, P u v <-> P v u) -> (forall u v, val u -- val v -> P u v) -> (forall u v, (val u == x) && val v -- y -> P u v) -> forall u v, u -- v -> P u v.
proof: Proof. move=> xNy Psym P1 P2 u v. rewrite smerge2edgeD //; case/or3P => //. exact: P1. exact: P2. rewrite Psym. exact: P2. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)