proposition: Lemma sskelP (G : graph2) (P : G -> G -> Prop) : Symmetric P -> (forall e : edge G, source e != target e -> P (source e) (target e)) -> (input != output :> G -> P input output) -> (forall x y : sskeleton G, x -- y -> P x y).
proof: Proof. move => S H IO x y. case/orP. exact: skelP. case/orP => /= /and3P [A /eqP ? /eqP ?];subst; first exact: IO. apply: S. exact: IO. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)