Nonnegative rationals #
This file defines the nonnegative rationals as a subtype of
Rat and provides its algebraic order
We also define an instance
CanLift ℚ ℚ≥0. This instance can be used by the
lift tactic to
x : ℚ and
hx : 0 ≤ x in the proof context with
x : ℚ≥0 while replacing all occurrences
↑x. This tactic also works for a function
f : α → ℚ with a hypothesis
hf : ∀ x, 0 ≤ f x.
The rational numbers are an algebra over the non-negative rationals.