proposition: Lemma Uplus_lt_compat_right : forall x y z:U, z <= [1-] y -> x < y -> (z + x) < (z + y).
proof: Proof. intros; setoid_rewrite (Uplus_sym z x). intros; setoid_rewrite (Uplus_sym z y). apply Uplus_lt_compat_left; auto. Qed.
imports: ALEA(Utheory)