Mizar/定義型/defpred

defpred P[Nat] means $1*($1-1);

P[n]≡n*(n-1);