proposition: Lemma seq_min_t r r' b (MAX: min_elt r b) (DOM: forall x y, r' x y -> x = b) : r ⁺ ⨾ r' ≡ ∅₂.
proof: Proof. eauto using seq_min with hahn. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid