search

coq-community / coq-100-theorems

Statements of famous theorems proven in Coq [maintainer=@jmadiot]
https://madiot.fr/coq100/
Other
55 stars 14 forks source link

[birthday.v] use stdlib lemmas to prove collision_count and enumerate_no_collisions #36

Open haansn08 opened 1 year ago

haansn08 commented 1 year ago

This PR refactors birthday.v to use definitions and lemmas already found in the standard library of Coq.