proposition: Lemma path_absorb_lt 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