proposition: Lemma min_sym : forall x y, min x y == min y x.
proof: Proof. intros; apply (Ule_total x y); intros; auto. rewrite min_eq_right; auto. rewrite min_eq_left; auto. rewrite min_eq_left; auto. rewrite min_eq_right; auto. Qed.
imports: ALEA(Utheory)