proposition: Lemma dom_change_compose x y: rel_on_dom (R @ S) x y <-> (rel_on_dom R @ rel_on_dom S) x y.
proof: Proof. intros; split; intro. ded (rel_on_dom_elim H). repeat destruct H0; destruct H1. unfold compose; ded (restriction H0); destruct H4. rewrite <- In_nats_decr_lt, (@element_at_exists A) in H5. destruct H5 as [z]. exists z. ded (element_at_in2 H1). ded (element_at_in2 H3). ded (element_at_in2 H5). unfold rel_on_dom. destruct H6; clear H9. destruct H7; clear H9. destruct H8; clear H9. ded (eq_In_find_first eq_dec H6); destruct H9; destruct H9. ded (eq_In_find_first eq_dec H7); destruct H11; destruct H11. ded (eq_In_find_first eq_dec H8); destruct H13; destruct H13. ded (nodup_unique Dom_nodup H1 H10). ded (nodup_unique Dom_nodup H3 H12). ded (nodup_unique Dom_nodup H5 H14). subst; rewrite H9, H11, H13; auto. unfold compose in H; destruct H as [z]; destruct H. unfold rel_on_dom in *. destruct (find_first (eq x) (eq_dec x)); auto with *. destruct (find_first (eq y) (eq_dec y)); auto with *. destruct (find_first (eq z) (eq_dec z)); auto with *. unfold compose; exists n1; auto with *. destruct (find_first (eq z) (eq_dec z));auto with *. Qed.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)