proposition: Lemma seq_wmin r r' b (MAX: wmin_elt r b) (D: forall x y, r' x y -> x = b) : r⨾ r' ⊆ r'.
proof: Proof. unfold seq; red; ins; desf; eauto. specialize (D _ _ H0); desf; apply MAX in H; desf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid