feat(library/data): add a few convenience lemmas

library/data/fin.lean

@@ -99,6 +99,9 @@ variable {n : nat}
 theorem val_lt : ∀ i : fin n, val i < n
 | (mk v h) := h
 
+lemma max_lt (i j : fin n) : max i j < n :=
+max_lt (is_lt i) (is_lt j)
+
 definition lift : fin n → Π m, fin (n + m)
 | (mk v h) m := mk v (lt_add_of_lt_right h m)
 

library/data/finset/basic.lean

@@ -6,7 +6,7 @@ Author: Leonardo de Moura, Jeremy Avigad
 Finite sets.
 -/
 import data.fintype.basic data.nat data.list.perm data.subtype algebra.binary
-open nat quot list subtype binary function
+open nat quot list subtype binary function eq.ops
 open [declarations] perm
 
 definition nodup_list (A : Type) := {l : list A | nodup l}
@@ -93,6 +93,9 @@ list.mem_singleton
 theorem mem_singleton_eq (x a : A) : (x ∈ singleton a) = (x = a) :=
 propext (iff.intro eq_of_mem_singleton (assume H, eq.subst H !mem_singleton))
 
+lemma eq_of_singleton_eq {a b : A} : singleton a = singleton b → a = b :=
+assume Pseq, eq_of_mem_singleton (Pseq ▸ mem_singleton a)
+
 definition decidable_mem [instance] [h : decidable_eq A] : ∀ (a : A) (s : finset A), decidable (a ∈ s) :=
 λ a s, quot.rec_on_subsingleton s
   (λ l, match list.decidable_mem a (elt_of l) with

library/data/list/set.lean

@@ -489,6 +489,10 @@ begin
   { exact mem_upto_succ_of_mem_upto (mem_upto_of_lt h')}
 end
 
+lemma upto_step : ∀ {n : nat}, upto (succ n) = (map succ (upto n))++[0]
+| 0        := rfl
+| (succ n) := begin rewrite [upto_succ n, map_cons, append_cons, -upto_step] end
+
 /- union -/
 section union
 variable {A : Type}