proposition: Lemma dot_edges (a b c d: Lv) (u v: Le): point (merge_seq (edge_graph a u b ⊎ edge_graph c v d) [:: (inl (inr tt), inr (inl tt))]) (\pi inl (inl tt)) (\pi (inr (inr tt))) ≃2 two_graph2 a d ∔ (b⊗c) ∔ [inl (inl tt), u, inr tt] ∔ [inr tt, v, inl (inr tt)].
proof: Proof. set G := (_ ⊎ _)%G. set H := (_ ∔ [_, _, _] ∔ [_,_,_])%G2. pose f (x : G) : H := match x with | inl (inl _) => inl (inl tt) | inr (inr _) => inl (inr tt) | _ => inr tt end. unshelve Iso2 (@merge_surj _ _ G _ H f (fun x => match x with | inl (inl _) => inl (inl tt) | inl (inr _) => inr (inr tt) | inr tt => inl (inr tt) end) (two_option_void) xpred0 _ _ _). 4,5: apply merge_surjE. - apply kernel_eqv_clot. * by repeat constructor. * case=>[[[]|[]]|[[]|[]]]; case=>[[[]|[]]|[[]|[]]]//= _; eqv. - by repeat case. - split. + by repeat case. + move => y. rewrite !big_sumType !big_unitType. by case: y ; [case; case | case]; rewrite /= ?monUl ?monU. + by repeat case. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2 rewriting)