proposition: Lemma Uplus_minus_assoc_right : forall x y z, y <= [1-]x -> z <= y -> x + (y - z) == (x + y) - z.
proof: Proof. intros; unfold Uminus. apply Oeq_trans with ([1-] (x + ([1-] (x + y) + z)) + x). rewrite Uplus_assoc. rewrite (Uplus_sym x ([1-] (x + y))). rewrite Uinv_plus_left; auto. rewrite Uinv_plus_left; auto. apply Ole_trans with ([1-] (x + y) + y); auto. Qed.
imports: ALEA(Utheory)