proposition: Lemma path_decomp_u_total r dom r' (T: is_total dom r') (DB: domb r' dom) (IRR: irreflexive (r＊ ⨾ r'⁺)) : (r ∪ r')⁺ ≡ r⁺ ∪ r＊ ⨾ r'⁺ ⨾ r＊.
proof: Proof. split; ins. { intros ? ? C; unfold seq, union in *. induction C; desf; eauto 8 using rt_refl, clos_trans; eauto 8 using clos_trans_in_rt, rt_trans. destruct (classic (z1 = z3)) as [|NEQ]; desf; eauto 6 using t_trans, rt_trans. eapply T in NEQ; desf. by exfalso; eauto 10 using clos_trans, rt_trans. by eauto 8 using clos_trans, rt_trans. by eapply t_rt_step in IHC0; desf; eauto. by eapply t_rt_step in IHC4; desf; eauto. } eapply inclusion_union_l; eauto with hahn. rewrite <- rt_ct with (r := r ∪ r'), <- ct_rt with (r := r ∪ r'); eauto 8 with hahn. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath