proposition: Lemma ct_union_singl A (r : relation A) a b : (r ∪ singl_rel a b)⁺ ≡ r⁺ ∪ r＊ ⨾ singl_rel a b ⨾ r＊.
proof: Proof. split. { unfold inclusion, union, singl_rel, seq. induction 1; desf; eauto 9 using clos_trans, clos_refl_trans, clos_trans_in_rt. } eapply inclusion_union_l; eauto with hahn. rewrite <- rt_ct, ct_begin; eauto with hahn. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath