proposition: Lemma path_specific_absorb A (r r' : relation A) : r ⨾ r' ⊆ r ⨾ r -> r' ⨾ r' ⊆ r' ⨾ r -> (r ∪ r')⁺ ⊆ r⁺ ∪ r' ⨾ r＊.
proof: Proof. ins. assert (r⁺ ⨾ r' ⊆ r⁺) by (by rewrite ct_end, !seqA, H, <- seqA; rewrite rt_unit at 1). apply inclusion_t_ind_right. - unionL. + unionR left. apply ct_step. + unionR right; basic_solver 25. - relsf; unionL. + by unionR left; rewrite ct_unit. + by unionR right; rewrite !seqA, rt_unit. + by unionR left; rewrite H1. + rewrite rtE at 1; relsf; unionL; unionR right. * by rewrite H0; arewrite (r ⊆ r＊) at 1. * by rewrite !seqA, H1, inclusion_t_rt. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath