proposition: Lemma insert_sorted: forall g a l, sorted g l -> sorted g (insert g a l).
proof: Proof. intros. induction H. simpl. apply sorted_1. simpl. destruct (Z.leb (elabel g a) (elabel g x)) eqn:ax. apply sorted_cons. apply Z.leb_le. auto. apply sorted_1. apply Z.leb_gt in ax. apply sorted_cons. lia. apply sorted_1. simpl. destruct (Z.leb (elabel g a) (elabel g x)) eqn:ax. apply sorted_cons. apply Z.leb_le. auto. apply sorted_cons; auto. apply Z.leb_gt in ax. simpl in IHsorted. destruct (Z.leb (elabel g a) (elabel g y)) eqn:ay. apply sorted_cons. lia. apply Z.leb_le in ay. apply sorted_cons; auto. apply Z.leb_gt in ay. apply sorted_cons. lia. apply IHsorted. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph CertiGraph.graph.undirected_graph