Theorem padicNorm.nat_lt_one_iff

Modification history