proposition: Lemma seq_rt_absorb_l r r' : r ⨾ r'＊ ⊆ r ∪ ((r ⨾ r') \ r) ⨾ r'＊.
proof: Proof. unfold seq, union, inclusion, minus_rel; ins; desf. induction H0 using clos_refl_trans_ind_left; desf; eauto. destruct (classic (r x z0)); eauto 8 using clos_refl_trans. right; repeat eexists; eauto using clos_refl_trans. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath