proposition: Lemma incl_SCC_list_fast i (Hi : i < dim) : Vnth (Vnth M Hi) Hi = true -> incl (SCC'_list i) (SCC_list_fast Hi).
proof: Proof. intros. assert(M[[i,i]] = true). unfold mat_unbound; destruct (le_gt_dec dim i). cut False; try tauto; lia. assert (g=Hi). unfold Peano.gt in *; apply lt_unique. subst; auto. unfold incl. intros. rewrite SCC'_list_exact in H1. unfold SCCTopoOrdering.SCC'_tag in H1. simpl in *. ded (find_first_exact _ _ _ H1). destruct H2 as [r]; destruct H2; destruct H3; destruct H3. subst a. unfold SCC_list_fast. eapply listfilter_in. eauto. rewrite <- H. apply list_of_vec_exact. destruct H4; ded (eq_In_find_first rule_eq_dec H4); do 2 destruct H6. assert (x<dim). eapply find_first_Some_bound. eauto. unfold SCC_list_fast. eapply listfilter_in. eauto. assert ((M[[i,x]]) = true). rewrite HM. ded (SCC_sym H3). clear H3. rename H9 into H3. rewrite (SCC_effective_exact hyps HM) in H3. unfold SCC_effective in H3. simpl in H3. unfold rel_on_dom in H3. simpl in *. rewrite H6 in H3. ded (eq_In_find_first rule_eq_dec H5). do 2 destruct H9. rewrite H9 in H3. assert (i=x0). eapply nodup_unique; eauto. subst x0. unfold GoM in H3. rewrite HM in H3. auto. unfold mat_unbound in H9; destruct (le_gt_dec dim i). cut False; try tauto; lia. destruct (le_gt_dec dim x). cut False; try tauto; lia. rewrite <- H9. unfold Peano.gt in *. assert (g=Hi). apply lt_unique. subst g; apply list_of_vec_exact. Qed.
imports: Coq(Permutation Multiset Setoid PermutSetoid) CoLoR(SCCTopoOrdering AGraph ATrs RelUtil RelSub BoundNat AdjMat LogicUtil NatUtil SCC SCC_dec ListExtras SN VecUtil GDomainBij OptUtil Union SortUtil ListNodup ListPermutation)