proposition: Lemma div_str_pos : forall a b, 0<b<=a -> 0 < a/b.
proof: Proof. intros a b (Hb,Hab). assert (LE : 0 <= a/b) by (apply div_pos; order). assert (MOD : a mod b < b) by (destruct (mod_bound_pos a b); order). rewrite lt_eq_cases in LE; destruct LE as [LT|EQ]; auto. exfalso; revert Hab. rewrite (div_mod a b), <-EQ; nzsimpl; order. Qed.
imports: NZAxioms NZMulOrder