proposition: Lemma path_ut_first r r' : (r ∪ r')⁺ ≡ r⁺ ∪ r＊ ⨾ r' ⨾ (r ∪ r')＊.
proof: Proof. split. - apply inclusion_t_ind_right. + apply inclusion_union_l. * apply inclusion_union_r; left; eauto with hahn. * apply inclusion_union_r; right; basic_solver 10. + relsf; repeat apply inclusion_union_l. * apply inclusion_union_r; left. unfold inclusion, seq; ins; desf; vauto. * apply inclusion_union_r; right. rewrite !seqA. arewrite (r ⊆ (r ∪ r')＊) at 3. rewrite rt_rt. done. * basic_solver 10. * apply inclusion_union_r; right. rewrite !seqA. arewrite (r' ⊆ (r ∪ r')＊) at 3. rewrite rt_rt. done. - arewrite (r ⊆ (r ∪ r')⁺) at 1. arewrite (r＊ ⊆ (r ∪ r')＊) at 1. arewrite (r' ⊆ (r ∪ r')⁺) at 3. rels. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath