proposition: Lemma wmin_elt_t : wmin_elt r a -> wmin_elt (r⁺) a.
proof: Proof. by red; ins; eapply wmin_elt_rt, inclusion_t_rt. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid