Further lemmas about the natural numbers #
The distinction between this file and
Mathlib.Data.Nat.Order.Basic is not particularly clear.
They are separated for now to minimize the porting requirements for tactics during the transition to
Mathlib.Data.Rat.Order has been ported,
please feel free to reorganize these two files.
instance Nat.Subtype.orderBot (s : Set ℕ) [inst : DecidablePred fun x => x ∈ s] [h : Nonempty ↑s] :
- Nat.Subtype.orderBot s = OrderBot.mk (_ : ∀ (x : ↑s), Nat.find (_ : ∃ a, a ∈ s) ≤ ↑x)
instance Nat.Subtype.semilatticeSup (s : Set ℕ) :
- One or more equations did not get rendered due to their size.
theorem Nat.dvd_left_injective :
Function.Injective fun x x_1 => x ∣ x_1
dvd is injective in the left argument