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