proposition: Lemma div_div : forall a b c, 0<=a -> 0<b -> 0<c -> (a/b)/c == a/(b*c).
proof: Proof. intros a b c Ha Hb Hc. apply div_unique with (b*((a/b) mod c) + a mod b); trivial. - destruct (mod_bound_pos (a/b) c), (mod_bound_pos a b); auto using div_pos. split. + apply add_nonneg_nonneg; auto. apply mul_nonneg_nonneg; order. + apply lt_le_trans with (b*((a/b) mod c) + b). * rewrite <- add_lt_mono_l; auto. * rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l; auto. - 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: NZAxioms NZMulOrder