proposition: Lemma wmin_elt_rt : wmin_elt r a -> wmin_elt (r＊) a.
proof: Proof. red; ins; apply clos_rt_rt1n in REL; induction REL; intuition; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid