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