Mul Valuation lt iff norm lt

lemma mulValuation_lt_iff_norm_lt {z a : ℚ_[p]} :    mulValuation z < mulValuation a ↔ ‖z‖ < ‖a‖ := by  rcases eq_or_ne a 0 with rfl | ha  · simp only [map_zero, norm_zero]    exact iff_of_false (not_lt.mpr zero_le) (not_lt.mpr (norm_nonneg _))  rcases eq_or_ne z 0 with rfl | hz  · simp [pos_iff_ne_zero, norm_pos_iff, ha]  · have hp1 : (1 : ℝ) < p := by exact_mod_cast (Fact.out : p.Prime).one_lt    rw [norm_eq_zpow_log_mulValuation hz, norm_eq_zpow_log_mulValuation ha,      zpow_lt_zpow_iff_right₀ hp1,      WithZero.log_lt_log ((mulValuation (p := p)).zero_iff.not.mpr hz)        ((mulValuation (p := p)).zero_iff.not.mpr ha)]