(*** le_plus *)
theorem nle_plus_bi (m1) (m2) (n1) (n2):
m1 ≤ m2 → n1 ≤ n2 → m1 + n1 ≤ m2 + n2.
/3 width=3 by nle_plus_bi_dx, nle_plus_bi_sn, nle_trans/ qed.
(*** le_plus *)
theorem nle_plus_bi (m1) (m2) (n1) (n2):
m1 ≤ m2 → n1 ≤ n2 → m1 + n1 ≤ m2 + n2.
/3 width=3 by nle_plus_bi_dx, nle_plus_bi_sn, nle_trans/ qed.