proposition: Lemma div_div : forall a b c, b~=0 -> 0<c -> (a/b)/c == a/(b*c).
proof: Proof. intros a b c Hb Hc. apply div_unique with (b*((a/b) mod c) + a mod b). - apply neg_pos_cases in Hb. destruct Hb as [Hb|Hb]. + right. destruct (mod_pos_bound (a/b) c), (mod_neg_bound a b); trivial. split. * apply le_lt_trans with (b*((a/b) mod c) + b). { now rewrite <- mul_succ_r, <- mul_le_mono_neg_l, le_succ_l. } now rewrite <- add_lt_mono_l. * apply add_nonpos_nonpos; trivial. apply mul_nonpos_nonneg; order. + left. destruct (mod_pos_bound (a/b) c), (mod_pos_bound a b); trivial. split. * apply add_nonneg_nonneg; trivial. apply mul_nonneg_nonneg; order. * apply lt_le_trans with (b*((a/b) mod c) + b). { now rewrite <- add_lt_mono_l. } now rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l. - rewrite (div_mod a b) at 1 by order. rewrite add_assoc, add_cancel_r. rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order. apply div_mod; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv