Compfiles/Russia1998P42.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Russian Mathematical Olympiad 1998, problem 42

A binary operation ⋆ on real numbers has the property that (a ⋆ b) ⋆ c = a + b + c.

Prove that a ⋆ b = a + b.

Imports (2)
Imported by 1 file
  1. problem Russia1998P42.russia1998_p42 line 33 source

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

    Statement uses: Real, Eq, HAdd.hAdd

    Proof uses: Trans.trans, Eq.symm, Eq.mpr, id, congrArg, Eq.refl, Eq.mp, propext, add_left_inj, OfNat.ofNat, add_comm, add_zero, HMul.hMul, Nat, two_mul, rfl, Ne, two_ne_zero, Iff.mp, mul_right_inj'

    59 instances, coercions and auxiliary constants left out.

    Tactic trace: 27 steps

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