proposition: Lemma comm_s_rt1 A (R S : rel A) : S@(R!1) << (R!1)@(S!1) -> (S!1)@(R!1) << (R!1)@(S!1).
proof: Proof. intros comm x y [z [H1 H2]]. induction H1 as [x z H | x y' z H H0 IH]. apply comm. exists z; split; hyp. assert (H1 := IH H2); clear IH H2. destruct H1 as [u [H2 H3]]. assert ((R!1 @ S!1) x u). apply comm. exists y'; split; hyp. destruct H1 as [m [xRm mSu]]. exists m; split. hyp. exact (tc1_trans mSu H3). Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)