for n being Nat holds Pitag_dist n is_metric_of REAL n