proposition: Lemma clos_trans_rotl A (r r' : relation A) : (r ⨾ r')⁺ ≡ r ⨾ (r' ⨾ r)＊ ⨾ r'.
proof: Proof. split; red; ins; unfold seq in *; desf. by induction H; desf; eauto 10 using clos_refl_trans. cut (exists m, clos_refl_trans (r ⨾ r') x m /\ r m z0); unfold seq in *. by ins; desf; eapply t_rt_step; eauto. clear H1; induction H0 using clos_refl_trans_ind_left; desf; eauto 8 using clos_refl_trans. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath