proposition: Lemma path_ut2 r r' (T: transitive r') : (r ∪ r')⁺ ≡ r⁺ ∪ r＊⨾ (r'⨾ r⁺)＊ ⨾ r'⨾ r＊.
proof: Proof. split. rewrite ct_end, path_ut; ins; relsf. rewrite !seqA, (rewrite_trans_seq_cr_l T), crE; relsf; hahn_rel. 2: by rewrite (rtE r) at 3; relsf. rewrite (rt_end (r' ⨾ r⁺)) at 1; relsf. rewrite <- ct_end, !seqA; hahn_rel. rewrite inclusion_t_rt with (r:=r) at 2; rewrite <- ct_end. rewrite inclusion_t_rt with (r:=r) at 2; hahn_rel. hahn_rel. rewrite inclusion_t_rt, <- (rt_ct (r ∪ r')); seq_rewrite <- ct_end. apply inclusion_seq_mon; eauto with hahn. apply inclusion_t_t2; rewrite ct_begin; eauto with hahn. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath