-- import data.subtype
open nat

check {x : nat| x > 0 }