Petri Net in Coq