Compfiles/Imo1972P3.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1972, Problem 3

Let m and n be non-negative integers. Prove that

(2m)!(2n)! / (m!n!(m + n)!)

is an integer.

Imports (3)
Imported by 1 file
  1. problem Imo1972P3.imo1972_p3 line 32 source

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

    Statement uses: Nat, Dvd.dvd, HMul.hMul, Nat.factorial, HAdd.hAdd, OfNat.ofNat

    Proof uses: HDiv.hDiv, Nat.recAux, Eq.mpr, id, Eq, congr, congrArg, mul_one, add_zero, Eq.trans, MulZeroClass.mul_zero, Exists.intro, Nat.choose, HSub.hSub, Eq.symm, Nat.choose_mul_factorial_mul_factorial, of_eq_true, HPow.hPow, True, Nat.rawCast and 120 more

    152 instances, coercions and auxiliary constants left out.

    Tactic trace: 41 steps

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