proposition: Lemma merge_union_can x : merge_union_bwd (merge_union_fwd x) = x %[mod e].
proof: Proof. case: x => /= => x. - by rewrite merge_union_bwdEl valK'. - case: (boolP (val x \in U)) => H. rewrite (merge_union_bwdEl H). + case: x H => x p H. exact: eqvI. + by rewrite (merge_union_bwdEr (valP x) H) valK'. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)