proposition: Lemma seq_wmin_t_singl r a b (MAX: wmin_elt r a) : r ⁺ ⨾ singl_rel a b ⊆ singl_rel a b.
proof: Proof. eauto using seq_wmin_singl with hahn. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid