proposition: Lemma ct_minus_transitive {A} (r r': relation A) (TR : transitive r) : r'⁺ \ r ⊆ (r' ∩ r)＊ ⨾ (r' \ r) ⨾ r'＊.
proof: Proof. ins. arewrite (r' ⊆ (r' ∩ r) ∪ (r' \ r)) at 1. { by unfolder; ins; desf; tauto. } rewrite path_ut_first, minus_union_l. unionL. { by arewrite (r' ∩ r ⊆ r); relsf. } arewrite ((r' ∩ r) ∪ (r' \ r) ⊆ r') at 1. basic_solver 12. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath