proposition: Lemma rt_union_singl A (r : relation A) a b : (r ∪ singl_rel a b)＊ ≡ r＊ ∪ r＊ ⨾ singl_rel a b ⨾ r＊.
proof: Proof. by rewrite rtE, rtE at 1; rewrite ct_union_singl, !unionA. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath