proposition: Theorem minus_le : forall a b c : nat, a <= b + c -> a - c <= b.
proof: Proof. intros a b c H; apply (fun p n m : nat => Nat.add_le_mono_l n m p) with (p := c). case (Nat.le_gt_cases a c); intros H1. replace (a - c) with 0; auto with arith. apply sym_equal; apply minus_O; auto with arith. rewrite Nat.add_comm, Nat.sub_add; auto with arith. rewrite Nat.add_comm; auto with arith. Qed.
imports: Coq(Arith ArithRing)