proposition: Lemma Uplus_lt_compat : forall x y z t:U, z <= [1-] x -> t <= [1-] y -> x < y -> z < t -> (x + z) < (y + t).
proof: Proof. intros; apply Ult_trans with (y + z); auto. apply Uplus_lt_compat_left; auto. apply Ole_trans with t; auto. Qed.
imports: ALEA(Utheory)