{α : Type u} →
  {motive : Std.Packages.LinearPreorderOfLEArgs α → Sort u_1} →
    ((toPreorderOfLEArgs : Std.Packages.PreorderOfLEArgs α) →
        (ord :
            let this := toPreorderOfLEArgs.le;
            let this := toPreorderOfLEArgs.decidableLE;
            Ord α) →
          (le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a) →
            (isLE_compare :
                let this := toPreorderOfLEArgs.le;
                let this_1 := toPreorderOfLEArgs.decidableLE;
                let this_2 := ord;
                ∀ (a b : α), (compare a b).isLE = true ↔ a ≤ b) →
              (isGE_compare :
                  let this := toPreorderOfLEArgs.le;
                  let this_1 := toPreorderOfLEArgs.decidableLE;
                  have this_2 := le_total;
                  let this_3 := ord;
                  ∀ (a b : α), (compare a b).isGE = true ↔ b ≤ a) →
                motive
                  { toPreorderOfLEArgs := toPreorderOfLEArgs, ord := ord, le_total := le_total,
                    isLE_compare := isLE_compare, isGE_compare := isGE_compare }) →
      (t : Std.Packages.LinearPreorderOfLEArgs α) → motive t