proposition: Lemma path_absorb_rt r r' (F: r'⨾ r ⊆ r \/ r'⨾ r ⊆ r') (T: transitive r') : (r ∪ r')⁺ ≡ r⁺ ∪ r＊ ⨾ r'.
proof: Proof. ins; rewrite path_absorb, rtE; relsf; hahn_rel. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath