proposition: Lemma wedge_eq_symm: forall x y, def_wedgerep x -> def_wedgerep y -> wedge_eq x y -> wedge_eq y x.
proof: Proof. intros. destruct H as [? [? ?]]. destruct H0 as [? [? ?]]. rewrite (surjective_pairing x) in *. rewrite (surjective_pairing y) in *. unfold wedge_eq in *. destruct x, y; simpl fst in *; simpl snd in *. destruct y, y0; trivial. lia. Qed.
imports: VST.floyd.proofauto Coq.ZArith.ZArith CertiGraph.floyd_ext.closed_lemmas CertiGraph.kruskal.kruskal_edgelist