proposition: Lemma path_union1 (r r': relation A) : (r ∪ r')⁺ ⊆ r'⁺ ∪ r'＊ ⨾ (r ∪ r ⨾ r'⁺)⁺.
proof: Proof. apply inclusion_t_ind_right. unionL; [|vauto]. by rewrite rtE; rewrite <- !ct_step; basic_solver 12. relsf; unionL; rewrite ?seqA. - unionR right. arewrite (r'⁺ ⊆ r'＊); hahn_frame. rewrite <- !ct_step; basic_solver 12. - by arewrite (r ⊆ (r ∪ r ⨾ r'⁺)＊) at 3; relsf. - arewrite (r'⁺ ⊆ r'＊) at 1. rewrite <- ct_end; basic_solver. - unionR right. rewrite ct_end, !seqA. arewrite ((r ∪ r ⨾ r'⁺) ⨾ r' ⊆ (r ∪ r ⨾ r'⁺)). relsf; unionL. * rewrite <- !ct_step; basic_solver 12. * rewrite !seqA. arewrite (r'⁺ ⊆ r'＊) at 1. rewrite <- ct_end; basic_solver. * relsf. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath