proposition: Lemma path_absorb2 r r' (F: r' ⨾ r ⊆ r) : (r ∪ r')⁺ ≡ r⁺ ∪ r'⁺ ∪ r⁺ ⨾ r'⁺.
proof: Proof. split; cycle 1. repeat apply inclusion_union_l; eauto with hahn. by repeat apply inclusion_seq_trans; eauto with hahn; vauto. apply inclusion_t_ind_left; relsf; repeat apply inclusion_union_l; eauto 10 using inclusion_r_t_t with hahn; try solve [rewrite (ct_begin r), <- !seqA, F, <- ct_begin; eauto 10 with hahn]. rewrite (ct_begin r) at 3; rewrite seqA; eauto 10 with hahn. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath