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'.