Mizar/定義型/defpred

出典: フリー教科書『ウィキブックス(Wikibooks)』
ナビゲーションに移動 検索に移動

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

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