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