proposition: Lemma seq_wmin_t r r' b (MAX: wmin_elt r b) (D: forall x y, r' x y -> x = b) : r ⁺⨾ r' ⊆ r'.
proof: Proof. eauto using seq_wmin with hahn. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid