proposition: Lemma seq_eq_max_rt r b (MAX: max_elt r b) : ⦗eq b⦘ ⨾ r＊ ≡ ⦗eq b⦘.
proof: Proof. rewrite rtE; relsf; rewrite seq_eq_max_t; relsf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid