proposition: Lemma Uminus_le_zero : forall x y, x <= y -> x - y == 0.
proof: Proof. unfold Uminus; intros. setoid_rewrite <- Uinv_one. apply Uinv_eq_compat. apply Ole_antisym; auto. apply Ole_trans with ([1-] y + y); auto. Qed.
imports: ALEA(Utheory)