have(Lean)
have: 補題を用意する - Lean by Example