proposition: Lemma ofnat_sub : forall n m, m<=n -> [n-m] == [n]-[m].
proof: Proof. intros n m H. rewrite ofnat_sub_r. revert n H. induction m. - intros. rewrite Nat.sub_0_r. now simpl. - intros. destruct n. + inversion H. + rewrite nat_rect_succ_r. simpl. etransitivity. * apply IHm; apply <- Nat.succ_le_mono; assumption. * eapply nat_rect_wd; [symmetry;apply pred_succ|apply pred_wd]. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat