for a being Int_position ex i being Nat st a = intpos i