proposition: Lemma rt_unionE A (r r' : relation A) : (r ∪ r')＊ ≡ r'＊ ⨾ (r ⨾ r'＊)＊.
proof: Proof. split; eauto 8 using inclusion_seq_rt, inclusion_rt_rt2 with hahn. apply inclusion_rt_ind_left; relsf; unionL; rels. rewrite <- seqA; rels; rewrite rtE at 2; relsf. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath