proposition: Lemma seq_min_r_eq r b (MAX: min_elt r b) : r^? ⨾⦗eq b⦘ ≡ ⦗eq b⦘.
proof: Proof. rewrite crE; relsf; rewrite seq_min_eq; relsf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid