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