add Coq proof practice