proposition: Lemma inclusion_seq_l r r1 r2 : r ⊆ r1 -> reflexive r2 -> r ⊆ r1 ⨾ r2.
proof: Proof. firstorder. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath