proposition: Theorem minus_plus_le : forall a b c d : nat, a <= c -> b <= d -> c + d - (a + b) = c - a + (d - b).
proof: Proof. intros a b c d H H0. apply Nat.add_sub_eq_l. apply trans_equal with (a + (c - a) + (b + (d - b))); auto with arith; ring. Qed.
imports: Coq(Arith ArithRing)