proposition: Lemma Uminus_plus_perm : forall x y z, y <= x -> z <= [1-]x -> x - y + z == x + z - y.
proof: Proof. intros; apply Uminus_eq_perm_right. apply Ole_trans with (y + z - y); auto. rewrite Uplus_minus_simpl_left; auto. apply Ole_trans with ([1-]x); auto. rewrite Uminus_perm. rewrite Uplus_minus_simpl_right; auto. Qed.
imports: ALEA(Utheory)