Proof of `An odd prime between n and 2n`

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Bertrand's postulate gives a prime $p$ with $n < p ≤ 2n$ . Since $n ≥ 2$ , this prime is not $2$ , hence odd.

Lax Lean Archive