proposition: Lemma compat_chain_dp_strict : forall a, succ (lhs a) (rhs a) -> chain_dp a << succ.
proof: Proof. unfold inclusion. intros. destruct H0. do 2 destruct H1. subst y. apply (absorbs_left_rtc Habsorb). exists (sub x0 (lhs a)). split. apply incl_elim with (R := int_red R #). 2: exact H1. apply rtc_incl. incl_trans (red R). apply int_red_incl_red. apply compat_red; hyp. destruct Hredord. apply H2. exact H. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)