proposition: Lemma Umult_simpl_right : forall x y z, ~0 == z -> (x * z) == (y * z) -> x == y.
proof: Proof. intros; apply Ole_antisym; auto. apply Umult_le_simpl_right with z; auto. apply Umult_le_simpl_right with z; auto. Qed.
imports: ALEA(Utheory)