proposition: Lemma s_SCC's_spec_cover i : i < dim -> In i s_SCC's.
proof: Proof. intros. unfold s_SCC's. destruct (sorted_SCC' hyps). unfold proj1_sig2. unfold permutation, meq in *. ded (p i). rewrite multiplicity_nats_decr_lt in H0. destruct (lt_ge_dec i (length (hyp_Dom hyps))); try lia. cut (exists j, j=i /\ In j x). intros; destruct H1. destruct H1. rewrite <- H1; auto. apply (multiplicity_in (@eq nat) eq_nat_dec). lia. assert (length (hyp_Dom hyps) = dim); intuition. 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)