theorem ZSpan.ceil_sub_mem_fundamentalDomain {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [LinearOrder K] [IsStrictOrderedRing K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (v : E) : ↑(ceil b v) - v ∈ fundamentalDomain b

theorem ZSpan.floor_eq_zero {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K] [LinearOrder K] [IsStrictOrderedRing K] [NormedAddCommGroup E] [NormedSpace K E] (b : Basis ι K E) [FloorRing K] [Fintype ι] (v : E) : v ∈ fundamentalDomain b ↔ floor b v = 0