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