proposition: Lemma le_exists_sub : forall n m, n<=m -> exists p, m == p+n /\ 0<=p.
proof: Proof. intros n m H. apply le_ind with (4:=H). - solve_proper. - exists 0; nzsimpl; split; order. - clear m H. intros m H (p & EQ & LE). exists (S p). split. + nzsimpl. now f_equiv. + now apply le_le_succ_r. Qed.
imports: NZAxioms NZBase NZMul NZOrder