proposition: Lemma hd_red_Mod_SCC'_hd_red_Mod_fast : forall i (Hi : i < dim), Vnth (Vnth M Hi) Hi = true -> hd_red_Mod_SCC' i << hd_red_Mod S (SCC_list_fast Hi).
proof: Proof. intros. eapply incl_trans. apply chain_SCC'_red_Mod. ded (incl_SCC_list_fast Hi H). unfold inclusion; intros. destruct H1 as [z]; exists z. destruct H1; split; auto. do 4 destruct H2. destruct H3. exists x0; exists x1; exists x2; split; try split; try tauto. apply H0. auto. 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)