proposition: Lemma flesh_out (G : sgraph) (sym0 : Le) (tt: Lv) (z : G) : { G' & (diso (sskeleton G') G * diso (skeleton G') G)%type}.
proof: Proof. pose G' := flesh_out_graph sym0 tt z. exists G'. suff iso : diso (skeleton G') G. { split=> //. rewrite <-iso. exact: iso_pointxx. } exists (bij_id : bij (skeleton G') G) => x y; rewrite /sk_rel. - case/andP=> _ /existsP[][/=][u v /=] uv. rewrite !inE /=. case/orP=> /andP[/eqP<- /eqP<-] //; by rewrite sg_sym. - move=> xy. rewrite /edge_rel/=/sk_rel sg_edgeNeq //=. apply/existsP; exists (Sub (x, y) xy). by rewrite !inE !eqxx. 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)