proposition: Lemma Uminus_assoc_right : forall x y z, y <= x -> z <= y -> x - (y - z) == (x - y) + z.
proof: Proof. intros. apply Uplus_eq_perm_left; auto. unfold Uminus at 1; apply Uinv_le_compat. apply Ole_trans with (1 - y + z); auto. apply Oeq_trans with ((y - z) + z + (x - y)). rewrite (Uminus_plus_simpl _ _ H0). rewrite (Uplus_sym y (x - y)); auto. norm_assoc_right; auto. Qed.
imports: ALEA(Utheory)