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