proposition: Lemma path_union (r r': relation A) : (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. - by unionR left; rewrite ct_unit. - by rewrite !seqA; rewrite <- ct_end; basic_solver 12. - rewrite (ct_step (r⁺ ⨾ r')). rewrite <- inclusion_t_rt at 1; basic_solver 22. - rewrite !seqA, inclusion_t_rt at 1. rewrite <- (ct_end (r＊ ⨾ r')); basic_solver 12. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath