Library Coqtail.Arith.Nle


Require Import Arith.
Require Import Compare.
Open Scope nat_scope.

Additional properties on le

elimination of le with plus
Lemma Nle_plus : n k, k n p, n = k + p.
intros n k.
intro.
induction H.
0. auto with arith.
destruct IHle.
rewrite H0.
(S x).
auto with arith.
Qed.