proposition: Lemma minus_seq_l 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