proposition: Lemma wmin_elt_r : wmin_elt r a -> wmin_elt (r^?) a.
proof: Proof. unfold clos_refl; red; ins; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid