michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/fin): add of_nat_to_nat theorem

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-07 17:46:47 -08:00
parent 98412ee942
commit 7b9758ac14
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/fin.lean
View file

@ -72,4 +72,10 @@ namespace fin
= succ (to_nat (of_nat p n _)) : rfl
... = succ p : to_nat_of_nat p n _
theorem of_nat_to_nat : ∀ {n : nat} (f : fin n) (h : to_nat f < n), of_nat (to_nat f) n h = f,
of_nat_to_nat (fz n) h := rfl,
of_nat_to_nat (@fs n f) h := calc
of_nat (to_nat (fs f)) (succ n) h = fs (of_nat (to_nat f) n _) : rfl
... = fs f : of_nat_to_nat f _
end fin