proposition: Lemma seq_wmin_t_eq r b (MAX: wmin_elt r b) : r ⁺ ⨾ ⦗eq b⦘ ⊆ ⦗eq b⦘.
proof: Proof. eauto using seq_wmin_eq with hahn. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid