proposition: Lemma uf_union_remains_disjoint1: forall (g1 g2: PreGraph Vertex Edge) (li1 : LstGraph g1 out_edge) (li2 : LstGraph g2 out_edge) (fin1: FiniteGraph g1) (fin2: FiniteGraph g2) (ma1: MathGraph g1 is_null) (ma2: MathGraph g2 is_null)u v a, vvalid g1 u -> vvalid g1 v -> vvalid g1 a -> uf_union g1 u v g2 -> ~ ufroot_same g1 a u -> ~ ufroot_same g1 a v -> ~ ufroot_same g2 a u.
proof: Proof. intros. pose proof (uf_union_create_precons _ _ _ _ _ _ H H0). destruct H5 as [u_rt [v_rt [? [? [? [? [? ?]]]]]]]. assert (ufroot_same g1 a a). { apply (ufroot_same_refl _ li1); trivial. } apply (uf_union_unaffected_inhabited _ _ _ _ _ _ _ _ H7 H8 H11 H9 H10) in H2. destruct H2 as [rt [? ?]]. intro. rewrite H12 in *. apply H3, (ufroot_same_uf_root_trans _ li2 a); trivial. - intro. apply (same_set_contra _ _ _ a H12); trivial. intro. apply H3. apply ufroot_same_symm; trivial. - intro. apply (same_set_contra _ _ _ a H12); trivial. intro. apply H4. apply ufroot_same_symm; trivial. - destruct H11 as [a_rt [? _]]. apply (ufroot_uf_set_in _ li1 a a_rt); trivial. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.Ensembles_ext CertiGraph.lib.EnumEnsembles CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable