proposition: Lemma Uinv_inv : forall x : U, [1-] [1-] x == x.
proof: Proof. intros; apply Oeq_trans with ([1-] (x + [1-] x) + x); auto. apply Oeq_sym; auto. setoid_rewrite (Uinv_opp_right x); setoid_rewrite Uinv_one; auto. Qed.
imports: ALEA(Utheory)