theorem Th8: :: HILB10_1:5
for a being non trivial Nat holds [a,1] = min_Pell's_solution_of ((a ^2) -' 1)