proposition: Lemma seq_min_eq r b (MAX: min_elt r b) : r ⨾⦗eq b⦘ ≡ ∅₂.
proof: Proof. eapply seq_min; unfold eqv_rel; ins; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid