proposition: Lemma dom_change_iter : forall n x y, rel_on_dom (iter (rel_on_nat R) n) x y <-> iter R n x y.
proof: Proof. induction n; intros; simpl. apply dom_change; auto. split; intros. rewrite dom_change_compose in H. unfold compose in *. destruct H as [z]; destruct H; exists z. rewrite dom_change in H; rewrite IHn in H0; auto with *. apply rel_on_nat_is_restricted. hyp. unfold compose in H; destruct H as [z]; destruct H. rewrite dom_change_compose. unfold compose; exists z; split. rewrite dom_change; hyp. rewrite IHn; hyp. apply rel_on_nat_is_restricted. hyp. Qed.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)