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.