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