Compfiles/Russia1995P10.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Russian Mathematical Olympiad 1995, problem 10

Let m, n be positive integers such that

gcd(m, n) + lcm(m, n) = m + n.

Show that one of the two numbers is divisible by the other.

Imports (3)
Imported by 1 file
  1. problem Russia1995P10.russia1995_p10 line 30 source

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

    Statement uses: Nat, And, Ne, OfNat.ofNat, Eq, HAdd.hAdd, GCDMonoid.gcd, GCDMonoid.lcm, Or, Dvd.dvd

    Proof uses: HDiv.hDiv, HMul.hMul, id, Not, HPow.hPow, Eq.mpr, congrArg, Eq.symm, Nat.left_distrib, pow_two, Nat.mul_div_cancel', dvd_trans, Nat.gcd_dvd_left, Nat.dvd_mul_right, Nat.add_comm, Eq.refl, HSub.hSub, Eq.mp, Int, Eq.trans and 16 more

    49 instances, coercions and auxiliary constants left out.

    Tactic trace: 33 steps

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