proposition: Lemma seq_max_t r r' b (MAX: max_elt r' b) (COD: forall x y, r x y -> y = b) : r⨾ r' ⁺ ≡ ∅₂.
proof: Proof. eauto using seq_max with hahn. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid