proposition: Lemma max_eq_mult : forall k x y, max (k*x) (k*y) == k * max x y.
proof: Proof. intros; apply Ole_antisym. apply max_le; auto. apply (max_eq_case (x:=x) (y:= y)); auto; intro H; rewrite H; auto. Qed.
imports: ALEA(Utheory)