proposition: Lemma rel_on_nat_is_restricted : is_restricted (rel_on_nat R) (nats_decr_lt (length Dom)).
proof: Proof. unfold is_restricted; intros. rewrite <- !In_nats_decr_lt; ded (rel_on_nat_elim x y H). repeat destruct H0; destruct H1. ded (element_at_in2 H1). ded (element_at_in2 H2). tauto. Qed.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)