-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.compare.fun_cases_unfolding : ∀ (motive : Float.Model.UnpackedFloat → Float.Model.UnpackedFloat → Option Ordering → Prop),
  (∀ (x : Float.Model.UnpackedFloat), motive Float.Model.UnpackedFloat.notANumber x none) →
    (∀ (x : Float.Model.UnpackedFloat),
        (x = Float.Model.UnpackedFloat.notANumber → False) → motive x Float.Model.UnpackedFloat.notANumber none) →
      (∀ (s₁ s₂ : Float.Model.UnpackedFloat.Sign),
          motive (Float.Model.UnpackedFloat.infinity s₁) (Float.Model.UnpackedFloat.infinity s₂)
            (some (compare s₁ 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
                  (some Ordering.gt)) →
          (∀ (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
                    (some Ordering.lt)) →
            (∀ (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)
                      (some Ordering.lt)) →
              (∀ (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)
                        (some Ordering.gt)) →
                (∀ (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) (some Ordering.gt)) →
                  (∀ (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) (some Ordering.lt)) →
                    (∀ (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)
                          (some Ordering.lt)) →
                      (∀ (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)
                            (some Ordering.gt)) →
                        (∀ (sign sign_1 : Float.Model.UnpackedFloat.Sign),
                            motive (Float.Model.UnpackedFloat.zero sign) (Float.Model.UnpackedFloat.zero sign_1)
                              (some Ordering.eq)) →
                          (∀ (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)
                                (some ((compare e₁ e₂).then (compare m₁ m₂)).swap)) →
                            (∀ (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)
                                  (some Ordering.lt)) →
                              (∀ (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)
                                    (some Ordering.gt)) →
                                (∀ (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)
                                      (some ((compare e₁ e₂).then (compare m₁ m₂)))) →
                                  ∀ (x x_1 : Float.Model.UnpackedFloat), motive x x_1 (x.compare x_1)