proposition: Lemma Umult_div_eq : forall x y z, ~0==y -> x*y==z -> x == z/y.
proof: Proof. intros; apply Umult_simpl_right with y; auto. assert (z<=y). apply Ole_trans with (x*y); auto. apply Oeq_trans with z; auto. apply Oeq_sym; auto. Qed.
imports: ALEA(Utheory)