proposition: Lemma Nle_plus : forall n k, k <= n -> exists p, n = k + p.
proof: Proof. intros n k. intro. induction H. exists 0. auto with arith. destruct IHle. rewrite H0. exists (S x). auto with arith. Qed.
imports: Arith Compare