proposition: Lemma edgeless_partial_lgraph: forall (g: UAdjMatGG), is_partial_lgraph edgeless_graph g.
proof: Proof. intros. split. unfold is_partial_graph. split. intros. simpl. simpl in H. rewrite vert_bound. auto. split. intros. pose proof (edgeless_graph_evalid e). contradiction. split. intros. pose proof (edgeless_graph_evalid e). contradiction. intros. pose proof (edgeless_graph_evalid e). contradiction. split. unfold preserve_vlabel; intros. destruct vlabel; destruct vlabel. auto. unfold preserve_elabel; intros. pose proof (edgeless_graph_evalid e). contradiction. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.find_lemmas CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.undirected_graph CertiGraph.graph.MathAdjMatGraph