proposition: Lemma seq_singl_max_t r a b (MAX: max_elt r b) : singl_rel a b ⨾ r⁺ ≡ ∅₂.
proof: Proof. eauto using seq_singl_max with hahn. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid