proposition: Lemma s_SCC's_spec_bound i : In i s_SCC's -> i < dim.
proof: Proof. intros. unfold s_SCC's in H. destruct (sorted_SCC' hyps). unfold proj1_sig2 in *. gen p; intros. unfold permutation, meq in p. ded (p i). rewrite multiplicity_nats_decr_lt in H0. destruct (lt_ge_dec i (length (hyp_Dom hyps))); try lia. assert (dim = length (hyp_Dom hyps)). auto. rewrite H1 in *; auto. cut (exists j, j=i /\ In j (nats_decr_lt dim)). intros; destruct H1. destruct H1. rewrite <- In_nats_decr_lt in H2. subst i; auto. eapply permutation_in. auto with typeclass_instances. apply permutation_sym. eauto. 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)