proposition: Lemma path_union2 (r r': relation A) : (r ∪ r')⁺ ⊆ r⁺ ∪ r'⁺ ⨾ r＊ ∪ r'＊ ⨾ (r⁺ ⨾ r'⁺)⁺ ⨾ r＊.
proof: Proof. rewrite path_union1; unionL. basic_solver 12. rewrite path_union. relsf. unionL. basic_solver 12. arewrite (r＊ ⨾ r ⊆ r⁺). basic_solver 12. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath