proposition: Lemma div_div : forall a b c, 0<b -> c~=0 -> (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). - rewrite abs_mul. destruct (mod_always_pos (a/b) c), (mod_always_pos a b); try order. split. + apply add_nonneg_nonneg; trivial. apply mul_nonneg_nonneg; order. + apply lt_le_trans with (b*((a/b) mod c) + abs b). * now rewrite <- add_lt_mono_l. * rewrite (abs_eq b) by order. 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