proposition: Theorem div_le_lower_bound: forall a b q, 0<=a -> 0<b -> b*q <= a -> q <= a/b.
proof: Proof. intros a b q Ha Hb H. destruct (lt_ge_cases 0 q). - rewrite <- (div_mul q b); try order. apply div_le_mono; auto. rewrite mul_comm; split; auto. apply lt_le_incl, mul_pos_pos; auto. - apply le_trans with 0; auto; apply div_pos; auto. Qed.
imports: NZAxioms NZMulOrder