1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21

variable[LE α][DecidableLE α][Std.IsLinearOrder α][BEq α][LawfulBEq α](l:List α)

@[grind]def I(n:α)
|[]=>[n]
|h::t=>ite (n≤h) (n::h::t) (h::I n t)

@[grind]def S:List α→List α
|[]=>[]
|h::t=>I h<|S t

@[grind]def D:List α→Prop
|[]|[_]=>True
|h::h'::t=>h≤h'∧D (h'::t)

theorem A:(D l→D (I n l))∧(n::l).Perm (I n l):=by induction l with
|nil=>grind
|cons _ t=>cases t<;>grind

example:D (S l)∧l.Perm (S l):=by induction l with
|nil=>grind
|cons h t=>grind [A (n:=h)<|S t]