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