{α : Type u_1} →
  [inst : PartialOrder α] →
    [decLE : DecidableLE α] →
      [decLT : DecidableLT α] →
        [decEq : DecidableEq α] → (∀ (a b : α), Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a b) → LinearOrder α