diff options
Diffstat (limited to 'theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v')
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 568ebeae86..e1dc5349bc 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -13,7 +13,7 @@ Require Import ZArith Nnat NAxioms NDiv NSig. Module NTypeIsNAxioms (Import N : NType'). Hint Rewrite - spec_0 spec_1 spec_succ spec_add spec_mul spec_pred spec_sub + spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub spec_div spec_modulo spec_gcd spec_compare spec_eq_bool spec_max spec_min spec_pow_pos spec_pow_N spec_pow spec_even spec_odd : nsimpl. @@ -37,6 +37,16 @@ Proof. intros. zify. generalize (spec_pos n); omega with *. Qed. +Theorem one_succ : 1 == succ 0. +Proof. +now zify. +Qed. + +Theorem two_succ : 2 == succ 1. +Proof. +now zify. +Qed. + Definition N_of_Z z := of_N (Zabs_N z). Section Induction. @@ -181,9 +191,6 @@ Qed. Program Instance pow_wd : Proper (eq==>eq==>eq) pow. -Local Notation "1" := (succ 0). -Local Notation "2" := (succ 1). - Lemma pow_0_r : forall a, a^0 == 1. Proof. intros. now zify. |