proposition: Lemma div_mul_cancel_r : forall a b c, b~=0 -> c~=0 -> (a*c)/(b*c) == a/b.
proof: Proof. intros a b c **. symmetry. apply div_unique with ((a mod b)*c). - destruct (lt_ge_cases 0 c). + rewrite <-(mul_0_l c), <-2mul_lt_mono_pos_r, <-2mul_le_mono_pos_r by trivial. now apply mod_bound_or. + rewrite <-(mul_0_l c), <-2mul_lt_mono_neg_r, <-2mul_le_mono_neg_r by order. destruct (mod_bound_or a b); tauto. - 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