proposition: Lemma div_mul_cancel_r : forall a b c, 0<=a -> 0<b -> 0<c -> (a*c)/(b*c) == a/b.
proof: Proof. intros a b c ? ? ?. symmetry. apply div_unique with ((a mod b)*c). - apply mul_nonneg_nonneg; order. - split. + apply mul_nonneg_nonneg; destruct (mod_bound_pos a b); order. + rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound_pos a b); auto. - rewrite (div_mod a b) at 1 by order. rewrite mul_add_distr_r. rewrite add_cancel_r. rewrite <- 2 mul_assoc. now rewrite (mul_comm c). Qed.
imports: NZAxioms NZMulOrder