proposition: Lemma filter_list_Permutation: forall {A:Type} {EA: EquivDec.EqDec A eq} (l1 l2: list A), NoDup l2 -> Permutation ((filter (fun x => in_dec EA x l1) l2) ++ (filter (fun x => negb (in_dec EA x l1)) l2)) l2.
proof: Proof. intros. apply NoDup_Permutation. apply NoDup_app_inv. apply NoDup_filter. auto. apply NoDup_filter. auto. intros. rewrite filter_In in H0. rewrite filter_In. destruct H0. unfold not; intros. destruct H2. destruct (in_dec EA x l1). inversion H3. inversion H1. auto. intros; split; intros. apply in_app_or in H0; destruct H0; rewrite filter_In in H0; destruct H0; auto. apply in_or_app. repeat rewrite filter_In. destruct (in_dec EA x l1). left; split; auto. right; split; auto. 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