proposition: Lemma commut_rtc : R# @ S << S @ R#.
proof: Proof. unfold incl. intros. do 2 destruct H. generalize x x0 H y H0. clear H0 y H x0 x. induction 1; intros. assert ((S @ R) x y0). apply commut. exists y. intuition. do 2 destruct H1. exists x0. intuition. exists y. intuition. ded (IHclos_refl_trans2 _ H1). do 2 destruct H2. ded (IHclos_refl_trans1 _ H2). do 2 destruct H4. exists x1. intuition. trans x0; hyp. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)