proposition: Lemma rtc_comp A (R S : rel A) : R# @ S << S U R! @ S.
proof: Proof. unfold incl. intros. do 2 destruct H. ded (rtc_split H). destruct H1. subst x0. left. exact H0. right. exists x0; split; hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)