proposition: Lemma ct_unionE A (r r' : relation A) : (r ∪ r')⁺ ≡ r'⁺ ∪ r'＊ ⨾ (r ⨾ r'＊)⁺.
proof: Proof. rewrite ct_begin, rt_unionE; relsf; rewrite <- seqA; rels. split; unionL; eauto using inclusion_seq_r, inclusion_seq_l with hahn. by rewrite rtE; relsf; unionL; eauto with hahn. by rewrite rtE at 1; relsf; unionL; eauto with hahn. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath