Compfiles/Canada1998P3.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Canadian Mathematical Olympiad 1998, Problem 3

Let n be a natural number such that n ≥ 2. Show that

(1/(n + 1))(1 + 1/3 + ... + 1/(2n - 1)) > (1/n)(1/2 + 1/4 + ... + 1/2n).

Imports (2)
Imported by 1 file
  1. problem Canada1998P3.canada1998_p3 line 27 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Real, HMul.hMul, HDiv.hDiv, Finset.sum, Finset.range, HAdd.hAdd

    Proof uses: Nat.le_induction, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.isNNRat_mul, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.rec, Finset.cons, Finset.notMem_range_self, Eq, Mathlib.Meta.NormNum.IsNNRat, Mathlib.Meta.NormNum.isNNRat_add, Mathlib.Meta.NormNum.isNNRat_div, Inv.inv, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.instAtLeastTwo and 151 more

    156 instances, coercions and auxiliary constants left out.

    Tactic trace: 35 steps

    Open to load the checked before-and-after goal states.