proposition: Lemma path_ut r r' (T: transitive r') : (r ∪ r')＊ ≡ r＊ ⨾ (r' ⨾ r⁺)＊ ⨾ r'^?.
proof: Proof. split. - apply inclusion_rt_ind; hahn_rel; eauto 4 with hahn hahn_full. apply transitiveI. rewrite crE at 1; relsf; unionL. hahn_frame_r; rewrite rtE with (r:=r' ⨾ r⁺) at 1; relsf; hahn_rel. hahn_frame_l; rewrite ct_end, !seqA; rels. by apply inclusion_seq_rt; ins; rewrite <- seqA, <- ct_begin; eauto with hahn. hahn_frame_l; rewrite rtE with (r:=r) at 1; relsf; hahn_rel; [|hahn_frame_r]. rewrite rtE with (r:=r' ⨾ r⁺) at 2; relsf; hahn_rel. hahn_frame_r; rewrite ct_begin with (r:=r' ⨾ r⁺); rewrite !seqA; relsf. by apply inclusion_seq_rt; ins; rewrite <- seqA, <- ct_begin; eauto with hahn. by apply inclusion_seq_rt; ins; rewrite <- seqA, <- ct_begin; eauto with hahn. - rewrite inclusion_t_rt. eauto 10 using inclusion_seq_trans, inclusion_rt_rt2 with hahn. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath