Commit 2021-10-11 06:17 957f64ee

View on Github →

feat(algebra/floor): When the floor is strictly positive (#9625) ⌊a⌋₊ and ⌊a⌋ are strictly positive iff 1 ≤ a. We use this to slightly golf IMO 2013 P5.

Estimated changes

Modified archive/imo/imo2013_q5.lean

Modified src/algebra/floor.lean

added theorem floor_pos

added theorem nat_floor_pos

added theorem sub_one_lt_nat_floor