Theorem Nat.choose_le_succ_of_lt_half_left

Modification history

2023-01-19 10:36
Mathlib/Data/Nat/Choose/Basic.lean
chore: format by line breaks with long lines (#1529) …
Modified Nat.choose_le_succ_of_lt_half_leftView on Github →
2022-12-17 08:57
Mathlib/Data/Nat/Choose/Basic.lean
feat port: Data.Nat.Choose.Basic (#1073) …
Added Nat.choose_le_succ_of_lt_half_leftView on Github →