proposition: Theorem Uplus_le_simpl_left : forall x y z : U, z <= [1-] x -> z + x <= z + y -> x <= y.
proof: Proof. intros. apply Uplus_le_simpl_right with z; auto. apply Ole_trans with (z + x); auto. apply Ole_trans with (z + y); auto. Qed.
imports: ALEA(Utheory)