proposition: Lemma K4_free_add_edge_sep_size2 (G : sgraph) (s1 s2 : G): K4_free G -> smallest vseparator [set s1; s2] -> s1 != s2 -> K4_free (add_edge s1 s2).
proof: Proof. move S12 : [set s1;s2] => S. move/esym in S12. move => K4free ssepS s1Ns2 K4G'. case: (vseparator_separation ssepS.1) => V1 [V2] [psep SV12]. wlog [phi rmapphi HphiV1] : {K4G'} V1 V2 psep SV12 / exists2 phi : K4 -> {set add_edge s1 s2}, minor_rmap phi & forall x : K4, phi x \subset V1. { move => W. case: (@separation_K4side (add_edge s1 s2) V1 V2) => //. - apply: add_edge_separation psep.1; by rewrite -SV12 S12 !inE eqxx. - rewrite -SV12 S12. apply: clique2. by rewrite /edge_rel/= !eqxx s1Ns2. - by rewrite -SV12 S12 cards2 s1Ns2. - move => phi map_phi [subV1|subV2]; first by apply: (W V1 V2) => //; exists phi. apply: (W V2 V1) => //; rewrite 1?proper_separation_symmetry 1?setIC //. by exists phi. } apply: K4free. apply: add_edge_rmap_separation_minor psep _ _ _ _ rmapphi HphiV1 => //. all: by rewrite -SV12. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries set_tac digraph) GraphTheory(sgraph treewidth minor connectivity)