mono_nat_update: make first argument implicit
This makes it consistent with the logic-level lemma, which is stated as
Lemma mono_nat_own_update {γ n} n' :
n ≤ n' →
mono_nat_auth_own γ 1 n ==∗ mono_nat_auth_own γ 1 n' ∗ mono_nat_lb_own γ n'.