proposition: Lemma seq_rt_absorb_r r r' : r＊ ⨾ r' ⊆ r' ∪ r＊ ⨾ ((r ⨾ r') \ r').
proof: Proof. apply inclusion_transpE. rewrite !transp_union, !transp_seq, !transp_minus, !transp_rt, !transp_seq; auto using seq_rt_absorb_l, transitive_transp. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath