proposition: Lemma Uplus_le_perm_left : forall x y z, x <= y + z -> x - y <= z.
proof: Proof. intros; apply (Ule_total y x); intros; auto. apply Uplus_le_simpl_left with y. unfold Uminus; setoid_rewrite (Uinv_inv ([1-] x + y)); auto. setoid_rewrite (Uplus_sym y (x-y)); rewrite (Uminus_plus_simpl x y); auto. apply Ole_trans with (0:U); auto. Qed.
imports: ALEA(Utheory)