[STATEMENT]
lemma pell_valuation_nonneg [simp]: "fst z \<ge> 0 \<Longrightarrow> snd z \<ge> 0 \<Longrightarrow> pell_valuation z \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> fst z; 0 \<le> snd z\<rbrakk> \<Longrightarrow> 0 \<le> pell_valuation z
[PROOF STEP]
by (auto simp: pell_valuation_def case_prod_unfold)