prob10:theory begin for_a:lemma forall(a:posreal,b:posreal,c:int,m:int,n:int):1 / a + 1 / b = 1 => c <= m * a & m * a < c + 1 => c <= n * b & n * b < c + 1 => c = m * a %|- for_a : PROOF %|- (then (skeep) %|- (spread (case "c < m * a") %|-…

theory prob10 imports Complex_Main "~~/src/HOL/Number_Theory/Primes" begin lemma for_a: fixes a b :: real and c m n :: int assumes "0 < a" and "0 < b" and "1 / a + 1 / b = 1" assumes "c <= m * a" and "m * a < c + 1" assumes "c <= n * b" an…