proposition: Lemma minus_seq_r r r' (T: transitive r') : (r ⨾ r') \ r' ⊆ (r \ r') ⨾ r'.
proof: Proof. unfold minus_rel, seq; red; ins; desf; repeat eexists; eauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath