theorem ADDC1: :: LIOUVIL1:2

for n being Nat holds n <= n !