proposition: Lemma Uplus_one_le : forall x y, x + y == 1 -> [1-] y <= x.
proof: Proof. intros; apply Ule_class; red; intros. assert (x < [1-] y); auto. assert (x + y < [1-] y + y); auto. assert (x + y < 1); auto. setoid_rewrite <- (Uinv_opp_left y); auto. Qed.
imports: ALEA(Utheory)