-(*** max_inv_O3 *)
-lemma nmax_inv_zero (n1) (n2): 𝟎 = (n1 ∨ n2) → ∧∧ 𝟎 = n1 & 𝟎 = n2.
-#n1 #n2 @(nat_ind_succ_2 … n1 n2) -n1 -n2 /2 width=1 by conj/
+lemma eq_inv_zero_nmax (n1) (n2): 𝟎 = (n1 ∨ n2) → ∧∧ 𝟎 = n1 & 𝟎 = n2.
+#n1 #n2 @(nat_ind_2_succ … n1 n2) -n1 -n2 /2 width=1 by conj/