proposition: Lemma Uplus_eq_simpl_right : forall x y z:U, z <= [1-] x -> z <= [1-] y -> (x + z) == (y + z) -> x == y.
proof: Proof. intros; apply Ole_antisym. apply Uplus_le_simpl_right with z; auto. apply Uplus_le_simpl_right with z; auto. Qed.
imports: ALEA(Utheory)