for n being Nat holds distance_by_norm_of (REAL-NS n) = Pitag_dist n