Demostrar que Si w, x, y, z \u2208 \u2115 tales que x \u2223 w, entonces x \u2223 yxz + x\u00b2 + w\u00b2<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport data.nat.gcd\n\nvariables w x y z : \u2115\n\nexample\n (h : x \u2223 w)\n : x \u2223 y * (x * z) + x^2 + w^2 :=\nsorry\n<\/pre>\n<\/p>\n
Soluciones con Lean<\/b><\/p>\n\nimport data.nat.gcd\n\nvariables w x y z : \u2115\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : x \u2223 w)\n : x \u2223 y * (x * z) + x^2 + w^2 :=\nbegin\n have h1 : x \u2223 x * z,\n by exact dvd.intro z rfl,\n have h2 : x \u2223 y * (x * z),\n by exact dvd_mul_of_dvd_right h1 y,\n have h3 : x \u2223 x^2,\n by apply dvd_mul_right,\n have h4 : x \u2223 w * w,\n by exact dvd_mul_of_dvd_left h w,\n have h5 : x \u2223 w^2,\n by rwa \u2190 pow_two w at h4,\n have h6 : x \u2223 y * (x * z) + x^2,\n by exact dvd_add h2 h3,\n show x \u2223 y * (x * z) + x^2 + w^2,\n by exact dvd_add h6 h5,\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : x \u2223 w)\n : x \u2223 y * (x * z) + x^2 + w^2 :=\nbegin\n apply dvd_add,\n { apply dvd_add,\n { apply dvd_mul_of_dvd_right,\n apply dvd_mul_right, },\n { rw pow_two,\n apply dvd_mul_right, }},\n { rw pow_two,\n apply dvd_mul_of_dvd_left h, },\nend\n<\/pre>\nSe puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\nReferencias<\/b><\/p>\n