proposition: Lemma path_ur r r' adom bdom (DA: doma r' adom) (DB: domb r' bdom) : (r ∪ r')⁺ ≡ r⁺ ∪ (r⁺ ⨾ ⦗adom⦘ ∪ r')⁺ ⨾ (⦗bdom⦘ ⨾ r⁺)^?.
proof: Proof. by ins; rewrite <- path_tur, ct_of_union_ct_l; eauto; vauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath