proposition: Lemma max_eq_plus_cte_right : forall x y k, max (x+k) (y+k) == (max x y) + k.
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)