proposition: Lemma Rquo_restricted : is_restricted Rquo (nats_decr_lt dim).
proof: Proof. unfold is_restricted. intros. rewrite <- !In_nats_decr_lt. unfold Rquo in H. do 2 destruct H. do 2 destruct H0. unfold SCC'_tag in *. split; eapply find_first_Some_bound; eauto. Qed.
imports: Coq(Permutation Multiset Heap PermutSetoid) CoLoR(AdjMat RelUtil ListExtras LogicUtil VecUtil NatUtil RelSub Path SortUtil ListNodup OptUtil BoundNat SCC SCC_dec Total)