proposition: Lemma seq_wmin_rt_eq r b (MAX: wmin_elt r b) : r ＊ ⨾ ⦗eq b⦘ ≡ ⦗eq b⦘.
proof: Proof. rewrite rtE; split; relsf; rewrite seq_wmin_t_eq; relsf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid