proposition: Lemma seq_ct_absorb_r r r' : r⁺ ⨾ r' ⊆ r' ∪ r＊ ⨾ ((r ⨾ r') \ r').
proof: Proof. rewrite <- seq_rt_absorb_r; eauto with hahn. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath