Note that AristotleLemmas section is AI-generated

Changes

1 changed files (+1/-0)

• Aristotle.lean
  • @@ -15,6 +15,7 @@ def Sorted : List α → Prop
    | [] | [_] => True | x :: x' :: xs => x ≤ x' ∧ Sorted (x' :: xs) + -- This section is AI-generated noncomputable section AristotleLemmas /-