-- Batteries.Data.Float.Lemmas
_private.Batteries.Data.Float.Lemmas.0.Float.Model.UnpackedFloat.compare.match_1.splitter : (motive : Float.Model.UnpackedFloat → Float.Model.UnpackedFloat → Sort u_1) →
  (x x_1 : Float.Model.UnpackedFloat) →
    ((x : Float.Model.UnpackedFloat) → motive Float.Model.UnpackedFloat.notANumber x) →
      ((x : Float.Model.UnpackedFloat) →
          (x = Float.Model.UnpackedFloat.notANumber → False) → motive x Float.Model.UnpackedFloat.notANumber) →
        ((s₁ s₂ : Float.Model.UnpackedFloat.Sign) →
            motive (Float.Model.UnpackedFloat.infinity s₁) (Float.Model.UnpackedFloat.infinity s₂)) →
          ((x : Float.Model.UnpackedFloat) →
              (x = Float.Model.UnpackedFloat.notANumber → False) →
                (∀ (s₂ : Float.Model.UnpackedFloat.Sign), x = Float.Model.UnpackedFloat.infinity s₂ → False) →
                  motive (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive) x) →
            ((x : Float.Model.UnpackedFloat) →
                (x = Float.Model.UnpackedFloat.notANumber → False) →
                  (∀ (s₂ : Float.Model.UnpackedFloat.Sign), x = Float.Model.UnpackedFloat.infinity s₂ → False) →
                    motive (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.negative) x) →
              ((x : Float.Model.UnpackedFloat) →
                  (x = Float.Model.UnpackedFloat.notANumber → False) →
                    (∀ (s₁ : Float.Model.UnpackedFloat.Sign), x = Float.Model.UnpackedFloat.infinity s₁ → False) →
                      motive x (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive)) →
                ((x : Float.Model.UnpackedFloat) →
                    (x = Float.Model.UnpackedFloat.notANumber → False) →
                      (∀ (s₁ : Float.Model.UnpackedFloat.Sign), x = Float.Model.UnpackedFloat.infinity s₁ → False) →
                        motive x (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.negative)) →
                  ((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)) →
                    ((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)) →
                      ((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)) →
                        ((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)) →
                          ((sign sign_1 : Float.Model.UnpackedFloat.Sign) →
                              motive (Float.Model.UnpackedFloat.zero sign) (Float.Model.UnpackedFloat.zero sign_1)) →
                            ((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)) →
                              ((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)) →
                                ((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)) →
                                  ((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)) →
                                    motive x x_1