proposition: Lemma div_mul_cancel_r : forall a b c, b~=0 -> 0<c -> (a*c)/(b*c) == a/b.
proof: Proof. intros. symmetry. apply div_unique with ((a mod b)*c). - rewrite abs_mul, (abs_eq c) by order. rewrite <-(mul_0_l c), <-mul_lt_mono_pos_r, <-mul_le_mono_pos_r by trivial. now apply mod_always_pos. - 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: ZAxioms ZMulOrder ZSgnAbs NZDiv