proposition: Lemma seq_rt_absorb_lt r r' (T: transitive r) : r ⨾ r'＊ ⊆ r ∪ r ⨾ (r' \ r) ⨾ r'＊.
proof: Proof. by rewrite seq_rt_absorb_l, minus_seq_l, seqA. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath