proposition: Lemma Uminus_zero_le : forall x y, x - y == 0 -> x <= y.
proof: Proof. intros x y; unfold Uminus; intros. setoid_rewrite <- (Uinv_inv x). apply Uplus_one_le. setoid_rewrite <- Uinv_zero; auto. setoid_rewrite <- H; auto. Qed.
imports: ALEA(Utheory)