`Compfiles/Imo1997P6.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

24 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1997, Problem 6

For each positive integer n, let f(n) denote the number of ways of representing n as a sum of powers of 2 with non-negative integer exponents. Representations which differ only in the ordering of their summands are considered to be the same. For example, f(4) = 4, because 4 can be represented as 4, 2 + 2, 2 + 1 + 1 or 1 + 1 + 1 + 1. Prove that for any integer n ≥ 3, 2^(n²/4) < f(2^n) < 2^(n²/2).

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo1997P6.f Documented declaration: f line 38 source
Source documentation
f n is the number of ways of representing n as a sum of powers of two with non-negative integer exponents, where representations that differ only in the order of their summands are considered the same. Rather than defining f as a cardinality, we define it directly through its classical recurrence: a representation of an odd number 2m + 1 must use a 1, hence f (2m + 1) = f (2m); a representation of 2m + 2 either uses a 1 (and deleting it gives a representation of 2m + 1) or does not (and halving every summand gives a representation of m + 1), hence f (2m + 2) = f (2m + 1) + f (m + 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, Imo1997P6.f.match_1, Unit, OfNat.ofNat, Nat.succ, HAdd.hAdd, dite, Eq, HMod.hMod, HDiv.hDiv, Not
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def f : ℕ → ℕ
  | 0 => 1
  | n + 1 => f n + if (n + 1) % 2 = 0 then f ((n + 1) / 2) else 0
termination_by n => n
decreasing_by all_goals lia

snip begin

/-- Unfolding equation for the recursive definition. -/
```
lemma Imo1997P6.f_succ Unfolding equation for the recursive definition line 47 source
Source documentation
Unfolding equation for the recursive definition.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1997P6.f, HAdd.hAdd, OfNat.ofNat, ite, HMod.hMod, HDiv.hDiv
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Imo1997P6.f.eq_2, eq_self
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma f_succ (n : ℕ) :
    f (n + 1) = f n + if (n + 1) % 2 = 0 then f ((n + 1) / 2) else 0 := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_odd A representation of an odd number must contain a 1 line 52 source
Source documentation
A representation of an odd number must contain a 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1997P6.f, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, ite, HMod.hMod, HDiv.hDiv, id, congrArg, Imo1997P6.f_succ, ite_eq_right, add_zero, Eq.refl
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma f_odd (m : ℕ) : f (2 * m + 1) = f (2 * m) := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_even The recurrence at even arguments line 56 source
Source documentation
The recurrence at even arguments.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1997P6.f, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, ite, HMod.hMod, HDiv.hDiv, id, congrArg, Imo1997P6.f_succ, add_assoc, Nat.add_mod_right, Nat.mul_mod_right, ite_eq_left, rfl, HAdd, Eq.rec, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma f_even (m : ℕ) : f (2 * m + 2) = f (2 * m + 1) + f (m + 1) := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_even' The recurrence at even arguments, shifted form line 62 source
Source documentation
The recurrence at even arguments, shifted form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Imo1997P6.f, HMul.hMul, HAdd.hAdd, HSub.hSub
Proof uses: Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, HAdd, Imo1997P6.f_even
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma f_even' (m : ℕ) (hm : 1 ≤ m) : f (2 * m) = f (2 * m - 1) + f m := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_zero line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Imo1997P6.f, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Imo1997P6.f.eq_1, eq_self
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P6.f_one line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Imo1997P6.f, OfNat.ofNat
Proof uses: Eq.mpr, HMul.hMul, id, congrArg, HAdd.hAdd, Imo1997P6.f_odd, Imo1997P6.f_zero
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P6.f_two line 71 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Imo1997P6.f, OfNat.ofNat
Proof uses: Eq.mpr, HAdd.hAdd, HMul.hMul, id, congrArg, Imo1997P6.f_even, Imo1997P6.f_one, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P6.f_three line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Imo1997P6.f, OfNat.ofNat
Proof uses: Eq.mpr, HMul.hMul, id, congrArg, HAdd.hAdd, Imo1997P6.f_odd, Imo1997P6.f_two
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P6.f_four line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Imo1997P6.f, OfNat.ofNat
Proof uses: Eq.mpr, HAdd.hAdd, HMul.hMul, id, congrArg, Imo1997P6.f_even, Imo1997P6.f_three, Imo1997P6.f_two, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P6.f_mono f is monotone nondecreasing line 82 source
Source documentation
f is monotone nondecreasing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monotone, Nat, Imo1997P6.f
Proof uses: monotone_nat_of_le_succ, Eq.mpr, LE.le, HAdd.hAdd, OfNat.ofNat, ite, Eq, HMod.hMod, HDiv.hDiv, id, congrArg, Imo1997P6.f_succ, Nat.le_add_right
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma f_mono : Monotone f := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_sum Iterating the recurrence gives f (2N) as a sum of values of f line 88 source
Source documentation
Iterating the recurrence gives f (2N) as a sum of values of f.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1997P6.f, HMul.hMul, OfNat.ofNat, Finset.sum, Finset.range, HAdd.hAdd
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, MulZeroClass.mul_zero, Imo1997P6.f_zero, Singleton.singleton, Finset, congrFun', zero_add, Finset.sum_singleton, eq_self, Eq.mpr, id, mul_add, mul_one, Imo1997P6.f_even, Imo1997P6.f_odd and 3 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma f_sum (N : ℕ) : f (2 * N) = ∑ i ∈ Finset.range (N + 1), f i := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_two_mul_lt The upper-bound engine: f (2m) is strictly less than (m + 1) * f m as soon as m ≥ 2 (the term f 0 = 1 < f m makes the inequality strict) line 97 source
Source documentation
The upper-bound engine: f (2m) is strictly less than (m + 1) * f m as soon as m ≥ 2 (the term f 0 = 1 < f m makes the inequality strict).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Imo1997P6.f, HMul.hMul, HAdd.hAdd
Proof uses: Eq, Finset.sum, Finset.range, Eq.mpr, HSMul.hSMul, Finset.card, id, congrArg, Finset.sum_const, Finset.card_range, smul_eq_mul, Eq.refl, Imo1997P6.f_sum, Finset.sum_lt_sum, Membership.mem, Finset, Imo1997P6.f_mono, Nat.le_of_lt_succ, Iff.mp, Nat.succ and 10 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma f_two_mul_lt (m : ℕ) (hm : 2 ≤ m) : f (2 * m) < (m + 1) * f m := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_pair_step The key pairing inequality for the lower bound: the pairs f k + f (2r + 1 - k) are nonincreasing in k for 1 ≤ k ≤ r line 110 source
Source documentation
The key pairing inequality for the lower bound: the pairs f k + f (2r + 1 - k) are nonincreasing in k for 1 ≤ k ≤ r.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HAdd.hAdd, Imo1997P6.f, HSub.hSub, HMul.hMul
Proof uses: Even, Odd, Or, Nat.even_or_odd, Eq, Eq.mpr, id, congrArg, Eq.symm, two_mul, Imo1997P6.f_odd, Nat.mul_sub, le_refl, Imo1997P6.f_even, Nat.add_sub_add_right, Nat.sub_add_eq, Imo1997P6.f_even', Imo1997P6.f_mono
43 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma f_pair_step (r k : ℕ) (hk : 1 ≤ k) (hkr : k < r) :
    f (k + 1) + f (2 * r - k) ≤ f k + f (2 * r + 1 - k) := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_pair_ge Every pair in the sum is at least 2 * f r line 121 source
Source documentation
Every pair in the sum is at least 2 * f r.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, Imo1997P6.f, HAdd.hAdd, HSub.hSub
Proof uses: Nat.recAux, Eq.mpr, id, Eq, congrArg, Nat.sub_zero, Nat.sub_add_comm, Nat.le_mul_of_pos_left, zero_lt_two, two_mul, Nat.add_sub_self_right, propext, Nat.add_le_add_iff_left, Imo1997P6.f_mono, Nat.le_add_right, Imo1997P6.f_pair_step, Trans.trans, rfl, Nat.le_of_succ_le, Eq.mp and 6 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma f_pair_ge (r k : ℕ) (hk : 1 ≤ k) (hkr : k ≤ r) :
    2 * f r ≤ f k + f (2 * r + 1 - k) := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_sum_pair The lemma `f 1 + f 2 + line 144 source
Source documentation
The lemma f 1 + f 2 + ... + f (2r) ≥ 2r * f r of the official solution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, Imo1997P6.f, Finset.sum, Finset.range, HAdd.hAdd
Proof uses: Eq, Eq.mpr, id, congrArg, two_mul, Finset.sum_range_add, Eq.refl, HSub.hSub, Eq.rec, Eq.trans, Eq.symm, Finset.sum_range_reflect, Finset.sum_congr, rfl, Finset, Membership.mem, LT.lt, Iff.mp, Finset.mem_range, Finset.sum_add_distrib and 26 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma f_sum_pair (r : ℕ) (hr : 1 ≤ r) :
    2 * r * f r ≤ ∑ i ∈ Finset.range (2 * r), f (i + 1) := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_lower_step The two-step lower-bound recurrence: f (2^(n+1)) > 2^n * f (2^(n-1)) line 166 source
Source documentation
The two-step lower-bound recurrence: f (2^(n+1)) > 2^n * f (2^(n-1)).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HMul.hMul, HPow.hPow, Imo1997P6.f, HSub.hSub, HAdd.hAdd
Proof uses: Eq, Finset.sum, Finset.range, Imo1997P6.f_sum, Eq.mp, congrArg, Eq.symm, pow_succ, mul_comm, Imo1997P6.f_sum_pair, Nat.one_le_two_pow, Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, Nat.sub_add_cancel, Imo1997P6.f_zero, Finset.sum_range_succ'
39 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma f_lower_step (n : ℕ) (hn : 1 ≤ n) :
    2 ^ n * f (2 ^ (n - 1)) < f (2 ^ (n + 1)) := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_lower_main The lower bound in integer form: (f (2^n))^4 > 2^(n²), proved by two-step induction; note 4 * (n + 2) + (n + 1)² = (n + 3)² line 182 source
Source documentation
The lower bound in integer form: (f (2^n))^4 > 2^(n²), proved by two-step induction; note 4 * (n + 2) + (n + 1)² = (n + 3)².

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HPow.hPow, Imo1997P6.f
Proof uses: Nat.strong_induction_on, Nat.casesAuxOn, HAdd.hAdd, of_eq_true, Eq.trans, True, congr, congrArg, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.one_natPow, Mathlib.Meta.NormNum.natPow_one, congrFun', Imo1997P6.f_two, eq_true_of_decide, Bool, Bool.true and 66 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma f_lower_main (n : ℕ) (hn : 1 ≤ n) : 2 ^ (n ^ 2) < (f (2 ^ n)) ^ 4 := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_sq_step One step of the upper-bound induction, in squared form line 201 source
Source documentation
One step of the upper-bound induction, in squared form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HPow.hPow, Imo1997P6.f, LT.lt, HAdd.hAdd
Proof uses: Trans.trans, Eq, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.natPow_one, Nat.pow_le_pow_right, Mathlib.Meta.NormNum.isNat_lt_true, Bool, Bool.false, HMul.hMul, Eq.mpr, id, congrArg, pow_succ, mul_comm, Imo1997P6.f_two_mul_lt, Nat.pow_lt_pow_left, Mathlib.Meta.NormNum.isNat_eq_false and 52 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma f_sq_step (n : ℕ) (hn : 2 ≤ n) (ih : (f (2 ^ n)) ^ 2 ≤ 2 ^ (n ^ 2)) :
    (f (2 ^ (n + 1))) ^ 2 < 2 ^ ((n + 1) ^ 2) := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_sq_le The upper bound in integer form, nonstrict version (for the induction) line 235 source
Source documentation
The upper bound in integer form, nonstrict version (for the induction).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HPow.hPow, Imo1997P6.f
Proof uses: Nat.le_induction, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit0, Imo1997P6.f_four, Mathlib.Meta.NormNum.IsNatPowT.trans, Eq, Nat.pow, eq_true, True.intro, le_of_lt and 2 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma f_sq_le (n : ℕ) (hn : 2 ≤ n) : (f (2 ^ n)) ^ 2 ≤ 2 ^ (n ^ 2) := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_sq_lt The upper bound in integer form, strict for n ≥ 3 line 241 source
Source documentation
The upper bound in integer form, strict for n ≥ 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HPow.hPow, Imo1997P6.f
Proof uses: HAdd.hAdd, HSub.hSub, Imo1997P6.f_sq_step, Nat.le_sub_one_of_lt, Imo1997P6.f_sq_le, Eq.mp, congrArg, Nat.sub_add_cancel
19 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma f_sq_lt (n : ℕ) (hn : 3 ≤ n) : (f (2 ^ n)) ^ 2 < 2 ^ (n ^ 2) := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_gt_lower The lower bound with real powers: 2^(n²/4) < f (2^n) line 246 source
Source documentation
The lower bound with real powers: 2^(n²/4) < f (2^n).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Real, HPow.hPow, HDiv.hDiv, Imo1997P6.f
Proof uses: Imo1997P6.f_lower_main, cast, Eq.symm, Eq.trans, congr, congrArg, Eq, Eq.mpr, id, Real.rpow_natCast, HMul.hMul, Real.rpow_mul, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, HPow and 47 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma f_gt_lower (n : ℕ) (hn : 3 ≤ n) :
    (2 : ℝ) ^ ((n : ℝ) ^ 2 / 4) < (f (2 ^ n) : ℝ) := by
…
```
Mentions: Imo1997P6.f
lemma Imo1997P6.f_lt_upper The upper bound with real powers: f (2^n) < 2^(n²/2) line 265 source
Source documentation
The upper bound with real powers: f (2^n) < 2^(n²/2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Real, Imo1997P6.f, HPow.hPow, HDiv.hDiv
Proof uses: Imo1997P6.f_sq_lt, cast, Eq.symm, Eq.trans, congr, congrArg, Eq, Eq.mpr, id, Real.rpow_natCast, HMul.hMul, Real.rpow_mul, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, HPow and 52 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma f_lt_upper (n : ℕ) (hn : 3 ≤ n) :
    (f (2 ^ n) : ℝ) < (2 : ℝ) ^ ((n : ℝ) ^ 2 / 2) := by
…
```
Mentions: Imo1997P6.f
problem Imo1997P6.imo1997_p6 line 285 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, And, LT.lt, Real, HPow.hPow, HDiv.hDiv, Imo1997P6.f
Proof uses: And.intro, Imo1997P6.f_gt_lower, Imo1997P6.f_lt_upper
34 instances, coercions and auxiliary constants left out.