proposition: Lemma comm_s_r A (R S : rel A) : S@R << (R!1)@(S#1) -> (R U S)#1 @ R @ (R U S)#1 << (R!1) @ (R U S)#1.
proof: Proof. intros comm x y [z2 [[z1 [xRSz1 z1Rz2]] z2RSy]]. induction xRSz1 as [ | m n z1 mRSn nRSz1 IH]. exists z2. split. apply t1_step. hyp. hyp. assert (((R!1) @ (R U S)#1) n y) as mRedy. apply IH. hyp. clear nRSz1 z1Rz2 z2RSy IH z1 z2. destruct mRedy as [o [nRo oRSy]]. induction mRSn. exists o. split; auto. apply t1_trans with n; hyp. destruct nRo as [o p oRp | o p q oRp pRq ]; assert (((R!1)@(S#1)) m p) as mRedp. apply comm; exists o; split; hyp. destruct mRedp as [x [mRx xSp]]. exists x. split. hyp. apply rtc1_preorder with p. apply union_rel_rt1_right. hyp. hyp. assert (((R!1)@(S#1)) m p) as mRedp. apply comm; exists o; split; hyp. destruct mRedp as [x [mRx xSp]]. exists x. split. hyp. hyp. destruct mRedp as [n [mRn sSp]]. exists n; split. hyp. apply rtc1_preorder with q. apply rtc1_preorder with p. apply union_rel_rt1_right. hyp. apply union_rel_rt1_left. apply tc1_incl_rtc1. hyp. hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)