proposition: Lemma max_elt_union : max_elt r a -> max_elt r' a -> max_elt (r +++ r') a.
proof: Proof. unfold union; red; ins; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid