proposition: Lemma path_ut_last r r' : (r ∪ r')⁺ ≡ r⁺ ∪ (r ∪ r')＊ ⨾ r' ⨾ r＊.
proof: Proof. split. - apply inclusion_t_ind_right. + unionL; [unionR left | unionR right]; unfolder; eauto using t_step, rt_refl. + relsf; unionL. * rewrite ct_end at 2; basic_solver 10. * rewrite !seqA; rewrite <- ct_end; basic_solver 10. * arewrite (r ⊆ (r ∪ r')); basic_solver 10. * arewrite (r ⊆ (r ∪ r')) at 2. arewrite (r' ⊆ (r ∪ r')＊) at 2. rels; basic_solver 10. - arewrite (r ⊆ (r ∪ r')⁺) at 1. arewrite (r ⊆ (r ∪ r')＊) at 3. arewrite (r' ⊆ (r ∪ r')⁺) at 3. rels. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath