(*** plus_le_0 *)
lemma nle_inv_plus_zero (m) (n): m + n ≤ 𝟎 → ∧∧ 𝟎 = m & 𝟎 = n.
/3 width=1 by nle_inv_zero_dx, eq_inv_zero_nplus/ qed-.
(*** plus_le_0 *)
lemma nle_inv_plus_zero (m) (n): m + n ≤ 𝟎 → ∧∧ 𝟎 = m & 𝟎 = n.
/3 width=1 by nle_inv_zero_dx, eq_inv_zero_nplus/ qed-.