proposition: Lemma wedge_le_refl: forall x, def_wedgerep x -> wedge_le x x.
proof: Proof. intros. destruct H as [? [? ?]]. unfold wedge_le. rewrite (surjective_pairing x). destruct (fst x); trivial. lia. Qed.
imports: VST.floyd.proofauto Coq.ZArith.ZArith CertiGraph.floyd_ext.closed_lemmas CertiGraph.kruskal.kruskal_edgelist