PF002K · theorem body

fermat_four_primitive_odd_even_descent

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Two actual primitive Pythagorean inversions and coprime square splittings construct a strictly smaller positive Fermat-four counterexample.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ a. ∀ b. ∀ h. PrimitiveFermatFourCounterexample(a,b,h) → Odd(a · a) → Even(b · b) → ∃ x. ∃ y. ∃ z. SmallerFermatFourCounterexample(x,y,z,h)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

ND0071 PrimitiveFermatFourCounterexample ND0072 SmallerFermatFourCounterexample PD0009 Even PD0010 Odd

In local proof propositions

CF0013 PrimitivePythagorean ND0070 EuclidParameters ND0072 SmallerFermatFourCounterexample PD0010 Odd
Exact expanded first-order statement
forall a b h. ((((~((a) = 0) /\ (~((b) = 0) /\ (~((h) = 0) /\ ((a) * (a) * (a) * (a) + (b) * (b) * (b) * (b) = (h) * (h)))))) /\ (forall pff_divisor_oriented_source. (exists pff_left_oriented_source. (a) = pff_divisor_oriented_source * pff_left_oriented_source) -> (exists pff_right_oriented_source. (b) = pff_divisor_oriented_source * pff_right_oriented_source) -> pff_divisor_oriented_source = 1))) -> (exists k. a * a = 2 * k + 1) -> (exists k. b * b = 2 * k) -> exists A B H. ((((~((A) = 0) /\ (~((B) = 0) /\ (~((H) = 0) /\ ((A) * (A) * (A) * (A) + (B) * (B) * (B) * (B) = (H) * (H)))))) /\ (exists ffd_gap_oriented_result. ffd_gap_oriented_result + S H = h)))

Proof neighborhood

Direct theorem prerequisites

PF002I fermat_four_primitive_square_triangle PF001X pythagorean_primitive_odd_even_inverse PF0025 fermat_four_square_nonzero PF002G fermat_four_nested_primitive_triangle PF0016 pythagorean_primitive_hypotenuse_odd PF002E fermat_four_odd_double_square_factors PF001U pythagorean_positive_even_leg_parameters_nonzero factor_nonzero_left · Stable closed PF0015 pythagorean_odd_square_has_odd_root PF002H fermat_four_second_parameter_descent

Direct theorem dependents

PF002L fermat_four_primitive_descent

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

127 script commands · 25 reading checkpoints · 9 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (9)
fermat four primitive square trianglepythagorean primitive odd even inversefermat four square nonzerofermat four nested primitive trianglepythagorean primitive hypotenuse oddfermat four odd double square factorspythagorean positive even leg parameters nonzeropythagorean odd square has odd rootfermat four second parameter descent
01Fix variables and assumptionsL1–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro h
  4. L4
    intro hprimitive
  5. L5
    intro haodd
  6. L6
    intro hbeven
02Separate the logical casesL7–10

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L7
    cases hprimitive
  2. L8
    cases hprimitive_left
  3. L9
    cases hprimitive_left_right
  4. L10
    cases hprimitive_left_right_right
03Establish htriangleL11–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply fermat four primitive square triangle.

  1. L11
    have htriangle : PrimitivePythagorean(a · a,b · b,h)Definitions: PrimitivePythagorean(a · a,b · b,h)Original native command in the exact edition
  2. L12
    apply fermat_four_primitive_square_triangle
  3. L13
    exact hprimitive
04Establish hfirstL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean primitive odd even inverse.

  1. L14
    have hfirst : ∃ m. ∃ n. EuclidParameters(a · a,b · b,h,m,n)Definitions: EuclidParameters(a · a,b · b,h,m,n)Original native command in the exact edition
  2. L15
    specialize pythagorean_primitive_odd_even_inverse (a * a)
  3. L16
    specialize pythagorean_primitive_odd_even_inverse (b * b)
  4. L17
    specialize pythagorean_primitive_odd_even_inverse (h)
  5. L18
    apply pythagorean_primitive_odd_even_inverse
  6. L19
    exact htriangle
  7. L20
    intro hzero
  8. L21
    specialize fermat_four_square_nonzero (a)
  9. L22
    apply fermat_four_square_nonzero
  10. L23
    exact hprimitive_left_left
05Use earlier factsL24–24

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L24
    exact hzero
06Fix variables and assumptionsL25–25

Work with arbitrary variables or the premises of the current implication.

  1. L25
    intro hzero
07Use earlier factsL26–31

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L26
    specialize fermat_four_square_nonzero (b)
  2. L27
    apply fermat_four_square_nonzero
  3. L28
    exact hprimitive_left_right_left
  4. L29
    exact hzero
  5. L30
    exact haodd
  6. L31
    exact hbeven
08Separate the logical casesL32–39

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L32
    cases hfirst
  2. L33
    cases hfirst_witness
  3. L34
    cases hfirst_witness_witness
  4. L35
    cases hfirst_witness_witness_right
  5. L36
    cases hfirst_witness_witness_right_right
  6. L37
    cases hfirst_witness_witness_right_right_right
  7. L38
    cases hfirst_witness_witness_right_right_right_right
  8. L39
    cases hfirst_witness_witness_right_right_right_right_right
09Establish hnestedL40–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply fermat four nested primitive triangle.

  1. L40
    have hnested : PrimitivePythagorean(a,x1,x)Definitions: PrimitivePythagorean(a,x1,x)Original native command in the exact edition
  2. L41
    specialize fermat_four_nested_primitive_triangle (a)
  3. L42
    specialize fermat_four_nested_primitive_triangle (x)
  4. L43
    specialize fermat_four_nested_primitive_triangle (x1)
  5. L44
    apply fermat_four_nested_primitive_triangle
  6. L45
    exact hfirst_witness_witness_right_right_left
  7. L46
    exact hfirst_witness_witness_right_right_right_right_right_left
10Establish hmoddL47–52

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean primitive hypotenuse odd.

  1. L47
  2. L48
    specialize pythagorean_primitive_hypotenuse_odd (a)
  3. L49
    specialize pythagorean_primitive_hypotenuse_odd (x1)
  4. L50
    specialize pythagorean_primitive_hypotenuse_odd (x)
  5. L51
    apply pythagorean_primitive_hypotenuse_odd
  6. L52
    exact hnested
11Establish hdoubleL53–60

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply fermat four odd double square factors.

  1. L53
    have hdouble : exists u v. (x = u * u /\ x1 = 2 * (v * v))
  2. L54
    specialize fermat_four_odd_double_square_factors (x)
  3. L55
    specialize fermat_four_odd_double_square_factors (x1)
  4. L56
    specialize fermat_four_odd_double_square_factors (b)
  5. L57
    apply fermat_four_odd_double_square_factors
  6. L58
    exact hfirst_witness_witness_right_right_left
  7. L59
    exact hmodd
  8. L60
    exact hfirst_witness_witness_right_right_right_right_right_right
12Separate the logical casesL61–63

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L61
    cases hdouble
  2. L62
    cases hdouble_witness
  3. L63
    cases hdouble_witness_witness
13Establish hparameterspositiveL64–73

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean positive even leg parameters nonzero.

  1. L64
    have hparameterspositive : ~(x = 0) /\ ~(x1 = 0)
  2. L65
    specialize pythagorean_positive_even_leg_parameters_nonzero (b * b)
  3. L66
    specialize pythagorean_positive_even_leg_parameters_nonzero (x)
  4. L67
    specialize pythagorean_positive_even_leg_parameters_nonzero (x1)
  5. L68
    apply pythagorean_positive_even_leg_parameters_nonzero
  6. L69
    intro hzero
  7. L70
    specialize fermat_four_square_nonzero (b)
  8. L71
    apply fermat_four_square_nonzero
  9. L72
    exact hprimitive_left_right_left
  10. L73
    exact hzero
14Use earlier factsL74–74

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L74
    exact hfirst_witness_witness_right_right_right_right_right_right
15Separate the logical casesL75–75

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L75
    cases hparameterspositive
16Establish hupositiveL76–84

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor nonzero left.

  1. L76
    have hupositive : ~(x2 = 0)
  2. L77
    intro hzero
  3. L78
    specialize factor_nonzero_left (x)
  4. L79
    specialize factor_nonzero_left (x2)
  5. L80
    specialize factor_nonzero_left (x2)
  6. L81
    apply factor_nonzero_left
  7. L82
    exact hparameterspositive_left
  8. L83
    exact hdouble_witness_witness_left
  9. L84
    exact hzero
17Establish hsecondL85–94

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pythagorean primitive odd even inverse.

  1. L85
    have hsecond : ∃ r. ∃ s. EuclidParameters(a,x1,x,r,s)Definitions: EuclidParameters(a,x1,x,r,s)Original native command in the exact edition
  2. L86
    specialize pythagorean_primitive_odd_even_inverse (a)
  3. L87
    specialize pythagorean_primitive_odd_even_inverse (x1)
  4. L88
    specialize pythagorean_primitive_odd_even_inverse (x)
  5. L89
    apply pythagorean_primitive_odd_even_inverse
  6. L90
    exact hnested
  7. L91
    exact hprimitive_left_left
  8. L92
    exact hfirst_witness_witness_left
  9. L93
    apply pythagorean_odd_square_has_odd_root
  10. L94
    exact haodd
18Construct an explicit witnessL95–95

Supply the displayed value, then prove that it has the required property.

  1. L95
    exists x3 * x3
19Use earlier factsL96–96

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L96
    exact hdouble_witness_witness_right
20Separate the logical casesL97–104

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L97
    cases hsecond
  2. L98
    cases hsecond_witness
  3. L99
    cases hsecond_witness_witness
  4. L100
    cases hsecond_witness_witness_right
  5. L101
    cases hsecond_witness_witness_right_right
  6. L102
    cases hsecond_witness_witness_right_right_right
  7. L103
    cases hsecond_witness_witness_right_right_right_right
  8. L104
    cases hsecond_witness_witness_right_right_right_right_right
21Establish hsmallerL105–114

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply fermat four second parameter descent.

  1. L105
    have hsmaller : ∃ A. ∃ B. SmallerFermatFourCounterexample(A,B,x2,h)Definitions: SmallerFermatFourCounterexample(A,B,x2,h)Original native command in the exact edition
  2. L106
    specialize fermat_four_second_parameter_descent (x2)
  3. L107
    specialize fermat_four_second_parameter_descent (x)
  4. L108
    specialize fermat_four_second_parameter_descent (x1)
  5. L109
    specialize fermat_four_second_parameter_descent (x3)
  6. L110
    specialize fermat_four_second_parameter_descent (x4)
  7. L111
    specialize fermat_four_second_parameter_descent (x5)
  8. L112
    specialize fermat_four_second_parameter_descent (h)
  9. L113
    apply fermat_four_second_parameter_descent
  10. L114
    exact hupositive
22Use earlier factsL115–121

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L115
    exact hfirst_witness_witness_left
  2. L116
    exact hsecond_witness_witness_right_right_left
  3. L117
    exact hdouble_witness_witness_left
  4. L118
    exact hdouble_witness_witness_right
  5. L119
    exact hsecond_witness_witness_right_right_right_right_left
  6. L120
    exact hsecond_witness_witness_right_right_right_right_right_right
  7. L121
    exact hfirst_witness_witness_right_right_right_right_left
23Separate the logical casesL122–123

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L122
    cases hsmaller
  2. L123
    cases hsmaller_witness
24Construct an explicit witnessL124–126

Supply the displayed value, then prove that it has the required property.

  1. L124
    exists x6
  2. L125
    exists x7
  3. L126
    exists x2
25Use earlier factsL127–127

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L127
    exact hsmaller_witness_witness

Library-wide reading audit

Original defined command ledger · 127 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004intro hprimitive
  5. 0005intro haodd
  6. 0006intro hbeven
  7. 0007cases hprimitive
  8. 0008cases hprimitive_left
  9. 0009cases hprimitive_left_right
  10. 0010cases hprimitive_left_right_right
  11. 0011have htriangle : PrimitivePythagorean(a · a,b · b,h)
    Exact native replay linehave htriangle : (((a * a) * (a * a) + (b * b) * (b * b) = (h) * (h)) /\ (forall pff_divisor_ffd_oriented_triangle. (exists pff_left_ffd_oriented_triangle. (a * a) = pff_divisor_ffd_oriented_triangle * pff_left_ffd_oriented_triangle) -> (exists pff_right_ffd_oriented_triangle. (b * b) = pff_divisor_ffd_oriented_triangle * pff_right_ffd_oriented_triangle) -> pff_divisor_ffd_oriented_triangle = 1))
  12. 0012apply fermat_four_primitive_square_triangle
  13. 0013exact hprimitive
  14. 0014have hfirst : ∃ m. ∃ n. EuclidParameters(a · a,b · b,h,m,n)
    Exact native replay linehave hfirst : exists m n. ((~((n) = 0) /\ ((exists pi_gap_ffd_first_inverse. pi_gap_ffd_first_inverse + S (n) = (m)) /\ ((forall pff_divisor_pi_ffd_first_inverse_coprime. (exists pff_left_pi_ffd_first_inverse_coprime. (m) = pff_divisor_pi_ffd_first_inverse_coprime * pff_left_pi_ffd_first_inverse_coprime) -> (exists pff_right_pi_ffd_first_inverse_coprime. (n) = pff_divisor_pi_ffd_first_inverse_coprime * pff_right_pi_ffd_first_inverse_coprime) -> pff_divisor_pi_ffd_first_inverse_coprime = 1) /\ (((((exists pp_even_pi_ffd_first_inverse_parity_first_even. (m) = 2 * pp_even_pi_ffd_first_inverse_parity_first_even) /\ (exists pp_odd_pi_ffd_first_inverse_parity_second_odd. (n) = 2 * pp_odd_pi_ffd_first_inverse_parity_second_odd + 1)) \/ ((exists pp_odd_pi_ffd_first_inverse_parity_first_odd. (m) = 2 * pp_odd_pi_ffd_first_inverse_parity_first_odd + 1) /\ (exists pp_even_pi_ffd_first_inverse_parity_second_even. (n) = 2 * pp_even_pi_ffd_first_inverse_parity_second_even)))) /\ ((h) = (m) * (m) + (n) * (n) /\ ((m) * (m) = (n) * (n) + (a * a) /\ (b * b) = 2 * ((m) * (n)))))))))
  15. 0015specialize pythagorean_primitive_odd_even_inverse (a * a)
  16. 0016specialize pythagorean_primitive_odd_even_inverse (b * b)
  17. 0017specialize pythagorean_primitive_odd_even_inverse (h)
  18. 0018apply pythagorean_primitive_odd_even_inverse
  19. 0019exact htriangle
  20. 0020intro hzero
  21. 0021specialize fermat_four_square_nonzero (a)
  22. 0022apply fermat_four_square_nonzero
  23. 0023exact hprimitive_left_left
  24. 0024exact hzero
  25. 0025intro hzero
  26. 0026specialize fermat_four_square_nonzero (b)
  27. 0027apply fermat_four_square_nonzero
  28. 0028exact hprimitive_left_right_left
  29. 0029exact hzero
  30. 0030exact haodd
  31. 0031exact hbeven
  32. 0032cases hfirst
  33. 0033cases hfirst_witness
  34. 0034cases hfirst_witness_witness
  35. 0035cases hfirst_witness_witness_right
  36. 0036cases hfirst_witness_witness_right_right
  37. 0037cases hfirst_witness_witness_right_right_right
  38. 0038cases hfirst_witness_witness_right_right_right_right
  39. 0039cases hfirst_witness_witness_right_right_right_right_right
  40. 0040have hnested : PrimitivePythagorean(a,x1,x)
    Exact native replay linehave hnested : (((a) * (a) + (x1) * (x1) = (x) * (x)) /\ (forall pff_divisor_ffd_oriented_nested. (exists pff_left_ffd_oriented_nested. (a) = pff_divisor_ffd_oriented_nested * pff_left_ffd_oriented_nested) -> (exists pff_right_ffd_oriented_nested. (x1) = pff_divisor_ffd_oriented_nested * pff_right_ffd_oriented_nested) -> pff_divisor_ffd_oriented_nested = 1))
  41. 0041specialize fermat_four_nested_primitive_triangle (a)
  42. 0042specialize fermat_four_nested_primitive_triangle (x)
  43. 0043specialize fermat_four_nested_primitive_triangle (x1)
  44. 0044apply fermat_four_nested_primitive_triangle
  45. 0045exact hfirst_witness_witness_right_right_left
  46. 0046exact hfirst_witness_witness_right_right_right_right_right_left
  47. 0047have hmodd : Odd(x)
    Exact native replay linehave hmodd : exists k. x = 2 * k + 1
  48. 0048specialize pythagorean_primitive_hypotenuse_odd (a)
  49. 0049specialize pythagorean_primitive_hypotenuse_odd (x1)
  50. 0050specialize pythagorean_primitive_hypotenuse_odd (x)
  51. 0051apply pythagorean_primitive_hypotenuse_odd
  52. 0052exact hnested
  53. 0053have hdouble : exists u v. (x = u * u /\ x1 = 2 * (v * v))
  54. 0054specialize fermat_four_odd_double_square_factors (x)
  55. 0055specialize fermat_four_odd_double_square_factors (x1)
  56. 0056specialize fermat_four_odd_double_square_factors (b)
  57. 0057apply fermat_four_odd_double_square_factors
  58. 0058exact hfirst_witness_witness_right_right_left
  59. 0059exact hmodd
  60. 0060exact hfirst_witness_witness_right_right_right_right_right_right
  61. 0061cases hdouble
  62. 0062cases hdouble_witness
  63. 0063cases hdouble_witness_witness
  64. 0064have hparameterspositive : ~(x = 0) /\ ~(x1 = 0)
  65. 0065specialize pythagorean_positive_even_leg_parameters_nonzero (b * b)
  66. 0066specialize pythagorean_positive_even_leg_parameters_nonzero (x)
  67. 0067specialize pythagorean_positive_even_leg_parameters_nonzero (x1)
  68. 0068apply pythagorean_positive_even_leg_parameters_nonzero
  69. 0069intro hzero
  70. 0070specialize fermat_four_square_nonzero (b)
  71. 0071apply fermat_four_square_nonzero
  72. 0072exact hprimitive_left_right_left
  73. 0073exact hzero
  74. 0074exact hfirst_witness_witness_right_right_right_right_right_right
  75. 0075cases hparameterspositive
  76. 0076have hupositive : ~(x2 = 0)
  77. 0077intro hzero
  78. 0078specialize factor_nonzero_left (x)
  79. 0079specialize factor_nonzero_left (x2)
  80. 0080specialize factor_nonzero_left (x2)
  81. 0081apply factor_nonzero_left
  82. 0082exact hparameterspositive_left
  83. 0083exact hdouble_witness_witness_left
  84. 0084exact hzero
  85. 0085have hsecond : ∃ r. ∃ s. EuclidParameters(a,x1,x,r,s)
    Exact native replay linehave hsecond : exists r s. ((~((s) = 0) /\ ((exists pi_gap_ffd_second_inverse. pi_gap_ffd_second_inverse + S (s) = (r)) /\ ((forall pff_divisor_pi_ffd_second_inverse_coprime. (exists pff_left_pi_ffd_second_inverse_coprime. (r) = pff_divisor_pi_ffd_second_inverse_coprime * pff_left_pi_ffd_second_inverse_coprime) -> (exists pff_right_pi_ffd_second_inverse_coprime. (s) = pff_divisor_pi_ffd_second_inverse_coprime * pff_right_pi_ffd_second_inverse_coprime) -> pff_divisor_pi_ffd_second_inverse_coprime = 1) /\ (((((exists pp_even_pi_ffd_second_inverse_parity_first_even. (r) = 2 * pp_even_pi_ffd_second_inverse_parity_first_even) /\ (exists pp_odd_pi_ffd_second_inverse_parity_second_odd. (s) = 2 * pp_odd_pi_ffd_second_inverse_parity_second_odd + 1)) \/ ((exists pp_odd_pi_ffd_second_inverse_parity_first_odd. (r) = 2 * pp_odd_pi_ffd_second_inverse_parity_first_odd + 1) /\ (exists pp_even_pi_ffd_second_inverse_parity_second_even. (s) = 2 * pp_even_pi_ffd_second_inverse_parity_second_even)))) /\ ((x) = (r) * (r) + (s) * (s) /\ ((r) * (r) = (s) * (s) + (a) /\ (x1) = 2 * ((r) * (s)))))))))
  86. 0086specialize pythagorean_primitive_odd_even_inverse (a)
  87. 0087specialize pythagorean_primitive_odd_even_inverse (x1)
  88. 0088specialize pythagorean_primitive_odd_even_inverse (x)
  89. 0089apply pythagorean_primitive_odd_even_inverse
  90. 0090exact hnested
  91. 0091exact hprimitive_left_left
  92. 0092exact hfirst_witness_witness_left
  93. 0093apply pythagorean_odd_square_has_odd_root
  94. 0094exact haodd
  95. 0095exists x3 * x3
  96. 0096exact hdouble_witness_witness_right
  97. 0097cases hsecond
  98. 0098cases hsecond_witness
  99. 0099cases hsecond_witness_witness
  100. 0100cases hsecond_witness_witness_right
  101. 0101cases hsecond_witness_witness_right_right
  102. 0102cases hsecond_witness_witness_right_right_right
  103. 0103cases hsecond_witness_witness_right_right_right_right
  104. 0104cases hsecond_witness_witness_right_right_right_right_right
  105. 0105have hsmaller : ∃ A. ∃ B. SmallerFermatFourCounterexample(A,B,x2,h)
    Exact native replay linehave hsmaller : exists A B. ((((~((A) = 0) /\ (~((B) = 0) /\ (~((x2) = 0) /\ ((A) * (A) * (A) * (A) + (B) * (B) * (B) * (B) = (x2) * (x2)))))) /\ (exists ffd_gap_oriented_smaller. ffd_gap_oriented_smaller + S x2 = h)))
  106. 0106specialize fermat_four_second_parameter_descent (x2)
  107. 0107specialize fermat_four_second_parameter_descent (x)
  108. 0108specialize fermat_four_second_parameter_descent (x1)
  109. 0109specialize fermat_four_second_parameter_descent (x3)
  110. 0110specialize fermat_four_second_parameter_descent (x4)
  111. 0111specialize fermat_four_second_parameter_descent (x5)
  112. 0112specialize fermat_four_second_parameter_descent (h)
  113. 0113apply fermat_four_second_parameter_descent
  114. 0114exact hupositive
  115. 0115exact hfirst_witness_witness_left
  116. 0116exact hsecond_witness_witness_right_right_left
  117. 0117exact hdouble_witness_witness_left
  118. 0118exact hdouble_witness_witness_right
  119. 0119exact hsecond_witness_witness_right_right_right_right_left
  120. 0120exact hsecond_witness_witness_right_right_right_right_right_right
  121. 0121exact hfirst_witness_witness_right_right_right_right_left
  122. 0122cases hsmaller
  123. 0123cases hsmaller_witness
  124. 0124exists x6
  125. 0125exists x7
  126. 0126exists x2
  127. 0127exact hsmaller_witness_witness