Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-17 00:58 c4125272

View on Github →

feat(data/list/sort): ordered_insert lemmas (#1437)

feat(data/list/sort): ordered_insert lemmas
add a lemma about L.tail.count

Estimated changes

Modified src/data/list/basic.lean

added theorem list.count_tail

Modified src/data/list/sort.lean

added theorem list.ordered_insert_count

added theorem list.ordered_insert_length

added theorem list.ordered_insert_nil

added theorem list.sorted.tail