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