proposition: Lemma rt_union_singl_max A (r : relation A) a b (MAX: max_elt r b) : (r ∪ singl_rel a b)＊ ≡ r＊ ⨾ (singl_rel a b) ^?.
proof: Proof. rewrite rt_union_singl, crE, seq_singl_max_rt; relsf. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath