proposition: Lemma Udiv_mult_assoc : forall x y z, x <= y*z -> x/(y*z) == (x/y)/z.
proof: Proof. intros; apply (Ueq_orc 0 z); auto; intros. rewrite (Udiv_by_zero (x/y)); auto. rewrite Udiv_by_zero; auto; rewrite <- H0; auto. intros; apply (Ueq_orc 0 y); auto; intros. rewrite (Udiv_by_zero x); auto. rewrite <-H1; auto. rewrite (Udiv_by_zero x); auto. rewrite <-H1; auto. apply Oeq_sym; apply Umult_div_eq; auto. rewrite (Umult_sym y z). apply Oeq_trans with (x / y / z * z * y); auto. assert (x/y <= z). apply Umult_div_le_right; auto. apply Ole_trans with (y*z); auto. rewrite (Udiv_mult (x/y) H0); auto. assert (x<=y); auto. apply Ole_trans with (y*z); auto. Qed.
imports: ALEA(Utheory)