-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.compare.match_1.congr_eq_4 : ∀ (motive : Float.Model.UnpackedFloat → Float.Model.UnpackedFloat → Sort u_1) (x x_1 : Float.Model.UnpackedFloat)
  (h_1 : (x : Float.Model.UnpackedFloat) → motive Float.Model.UnpackedFloat.notANumber x)
  (h_2 : (x : Float.Model.UnpackedFloat) → motive x Float.Model.UnpackedFloat.notANumber)
  (h_3 :
    (s₁ s₂ : Float.Model.UnpackedFloat.Sign) →
      motive (Float.Model.UnpackedFloat.infinity s₁) (Float.Model.UnpackedFloat.infinity s₂))
  (h_4 :
    (x : Float.Model.UnpackedFloat) →
      motive (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive) x)
  (h_5 :
    (x : Float.Model.UnpackedFloat) →
      motive (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.negative) x)
  (h_6 :
    (x : Float.Model.UnpackedFloat) →
      motive x (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive))
  (h_7 :
    (x : Float.Model.UnpackedFloat) →
      motive x (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.negative))
  (h_8 :
    (mantissa : ℕ) →
      (exponent : ℤ) →
        (mantissa_pos : 0 < mantissa) →
          (sign : Float.Model.UnpackedFloat.Sign) →
            motive
              (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent mantissa_pos)
              (Float.Model.UnpackedFloat.zero sign))
  (h_9 :
    (mantissa : ℕ) →
      (exponent : ℤ) →
        (mantissa_pos : 0 < mantissa) →
          (sign : Float.Model.UnpackedFloat.Sign) →
            motive
              (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa exponent mantissa_pos)
              (Float.Model.UnpackedFloat.zero sign))
  (h_10 :
    (sign : Float.Model.UnpackedFloat.Sign) →
      (mantissa : ℕ) →
        (exponent : ℤ) →
          (mantissa_pos : 0 < mantissa) →
            motive (Float.Model.UnpackedFloat.zero sign)
              (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent mantissa_pos))
  (h_11 :
    (sign : Float.Model.UnpackedFloat.Sign) →
      (mantissa : ℕ) →
        (exponent : ℤ) →
          (mantissa_pos : 0 < mantissa) →
            motive (Float.Model.UnpackedFloat.zero sign)
              (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa exponent mantissa_pos))
  (h_12 :
    (sign sign_1 : Float.Model.UnpackedFloat.Sign) →
      motive (Float.Model.UnpackedFloat.zero sign) (Float.Model.UnpackedFloat.zero sign_1))
  (h_13 :
    (m₁ : ℕ) →
      (e₁ : ℤ) →
        (mantissa_pos : 0 < m₁) →
          (m₂ : ℕ) →
            (e₂ : ℤ) →
              (mantissa_pos_1 : 0 < m₂) →
                motive (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative m₁ e₁ mantissa_pos)
                  (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative m₂ e₂ mantissa_pos_1))
  (h_14 :
    (mantissa : ℕ) →
      (exponent : ℤ) →
        (mantissa_pos : 0 < mantissa) →
          (mantissa_1 : ℕ) →
            (exponent_1 : ℤ) →
              (mantissa_pos_1 : 0 < mantissa_1) →
                motive
                  (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa exponent
                    mantissa_pos)
                  (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa_1 exponent_1
                    mantissa_pos_1))
  (h_15 :
    (mantissa : ℕ) →
      (exponent : ℤ) →
        (mantissa_pos : 0 < mantissa) →
          (mantissa_1 : ℕ) →
            (exponent_1 : ℤ) →
              (mantissa_pos_1 : 0 < mantissa_1) →
                motive
                  (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent
                    mantissa_pos)
                  (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa_1 exponent_1
                    mantissa_pos_1))
  (h_16 :
    (m₁ : ℕ) →
      (e₁ : ℤ) →
        (mantissa_pos : 0 < m₁) →
          (m₂ : ℕ) →
            (e₂ : ℤ) →
              (mantissa_pos_1 : 0 < m₂) →
                motive (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive m₁ e₁ mantissa_pos)
                  (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive m₂ e₂ mantissa_pos_1))
  (x_2 : Float.Model.UnpackedFloat),
  x = Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive →
    x_1 = x_2 →
      (x_2 = Float.Model.UnpackedFloat.notANumber → False) →
        (∀ (s₂ : Float.Model.UnpackedFloat.Sign), x_2 = Float.Model.UnpackedFloat.infinity s₂ → False) →
          (match x, x_1 with
            | Float.Model.UnpackedFloat.notANumber, x => h_1 x
            | x, Float.Model.UnpackedFloat.notANumber => h_2 x
            | Float.Model.UnpackedFloat.infinity s₁, Float.Model.UnpackedFloat.infinity s₂ => h_3 s₁ s₂
            | Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive, x => h_4 x
            | Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.negative, x => h_5 x
            | x, Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive => h_6 x
            | x, Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.negative => h_7 x
            | Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent mantissa_pos,
              Float.Model.UnpackedFloat.zero sign => h_8 mantissa exponent mantissa_pos sign
            | Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa exponent mantissa_pos,
              Float.Model.UnpackedFloat.zero sign => h_9 mantissa exponent mantissa_pos sign
            | Float.Model.UnpackedFloat.zero sign,
              Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent mantissa_pos =>
              h_10 sign mantissa exponent mantissa_pos
            | Float.Model.UnpackedFloat.zero sign,
              Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa exponent mantissa_pos =>
              h_11 sign mantissa exponent mantissa_pos
            | Float.Model.UnpackedFloat.zero sign, Float.Model.UnpackedFloat.zero sign_1 => h_12 sign sign_1
            | Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative m₁ e₁ mantissa_pos,
              Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative m₂ e₂ mantissa_pos_1 =>
              h_13 m₁ e₁ mantissa_pos m₂ e₂ mantissa_pos_1
            | Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa exponent mantissa_pos,
              Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa_1 exponent_1
                mantissa_pos_1 =>
              h_14 mantissa exponent mantissa_pos mantissa_1 exponent_1 mantissa_pos_1
            | Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent mantissa_pos,
              Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa_1 exponent_1
                mantissa_pos_1 =>
              h_15 mantissa exponent mantissa_pos mantissa_1 exponent_1 mantissa_pos_1
            | Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive m₁ e₁ mantissa_pos,
              Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive m₂ e₂ mantissa_pos_1 =>
              h_16 m₁ e₁ mantissa_pos m₂ e₂ mantissa_pos_1) ≍
            h_4 x_2