proposition: Lemma le_plus_le : forall a b c d : nat, a <= b -> a + c = b + d -> d <= c.
proof: Proof. intros. cut (c = b - a + d). intros H1; rewrite H1. auto with arith. apply Nat.add_cancel_l with (p := a); auto. rewrite Nat.add_assoc. rewrite (Nat.add_comm a (b - a)). rewrite Nat.sub_add; auto. Qed.
imports: Coq(Arith ArithRing)