theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 → m1 ≤ m2
→ n1 + m1 ≤ n2 + m2.
#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 → m1 ≤ m2
→ n1 + m1 ≤ n2 + m2.
#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))