proposition: Lemma ct_union_singl_max A (r : relation A) a b (MAX: max_elt r b) : (r ∪ singl_rel a b)⁺ ≡ r⁺ ∪ r＊ ⨾ singl_rel a b.
proof: Proof. rewrite ct_union_singl, seq_singl_max_rt; ins. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath