scheme :: COMPTRIG:sch 1
Regrwithout0{ P₁[ Nat] } :

P₁[1]

provided

A1: ex k being non zero Nat st P₁[k] and
A2: for k being non zero Nat st k <> 1 & P₁[k] holds
ex n being non zero Nat st
( n < k & P₁[n] )