theorem Nat.self_sub_floor_lt_one {R : Type u_1} [Ring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (x : R) : x - ↑⌊x⌋₊ < 1

theorem Nat.zero_le_self_sub_floor {R : Type u_1} [Ring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {x : R} (hx : 0 ≤ x) : 0 ≤ x - ↑⌊x⌋₊

theorem pow_two_mul_abs {α : Type u_1} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (n : ℕ) (a : α) : |a| ^ (2 * n) = a ^ (2 * n)