/2 width=3 by nle_trans/ qed.
(* Main constructions with nplus ********************************************)
/2 width=3 by nle_trans/ qed.
(* Main constructions with nplus ********************************************)
(*** 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-.