proposition: Lemma Uplus_minus_perm_le : forall x y z, x + z - y <= x - y + z.
proof: Proof. intros; apply (Ule_total y x); auto; intro. apply (Ule_total z ([1-]x)); auto; intro. rewrite Uminus_plus_perm; auto. rewrite (Uplus_one x z); auto. apply Ole_trans with (x - y + [1-]x); auto. unfold Uminus at 2. rewrite Uinv_plus_left; auto. Qed.
imports: ALEA(Utheory)