In this doc link there are useful theorems about division. I tried importing it using Require Import in CoqIDE 8.9.0, however while the import succeeds, the following code fails with The reference div_lt_upper_bound was not found in the current environment.
Require Import Coq.Numbers.NatInt.NZDiv.
Check div_lt_upper_bound.
I tried downloading the source code for the file and manually importing it via Load, but then I get the following message with no further explanation (the first line is in red):
Application of a functor with too few arguments.
Interactive Module Type DivMod started
div is declared
modulo is declared
Module Type DivMod is defined
Interactive Module Type DivModNotation started
Module Type DivModNotation is defined
Module Type DivMod' is defined
Interactive Module Type NZDivSpec started
div_mod is declared
mod_bound_pos is declared
Module Type NZDivSpec is defined
Module Type NZDiv is defined
How do I load those theorems properly? Why did the previous methods not work?
The quick answer is that you are looking at the Module Type (see Print NZDivProp.).
The actual usage is simple, e. g.
Require Import Arith.
Check Nat.div_lt_upper_bound.
(*
Nat.div_lt_upper_bound
: forall a b q : nat, b <> 0 -> a < b * q -> a / b < q
*)