proposition: Lemma Umult_div_assoc : forall x y z, y <= z-> (x*y) / z == x * (y/z).
proof: Proof. intros; apply (Ueq_orc 0 z); auto; intros. repeat rewrite Udiv_by_zero; auto. apply Oeq_sym; apply Umult_div_eq; auto. apply Oeq_trans with (x * (y / z * z)); auto. Qed.
imports: ALEA(Utheory)