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