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