diff options
Diffstat (limited to 'theories/Ints/BigN.v')
| -rw-r--r-- | theories/Ints/BigN.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/theories/Ints/BigN.v b/theories/Ints/BigN.v index d7b406d3de..e8b92186bd 100644 --- a/theories/Ints/BigN.v +++ b/theories/Ints/BigN.v @@ -113,3 +113,13 @@ Notation " i * j " := (BigN.mul i j) : bigN_scope. Notation " i / j " := (BigN.div i j) : bigN_scope. Notation " i ?= j " := (BigN.compare i j) : bigN_scope. + Theorem succ_pred: forall q, + (0 < BigN.to_Z q -> + BigN.to_Z (BigN.succ (BigN.pred q)) = BigN.to_Z q)%Z. + intros q Hq. + rewrite BigN.spec_succ. + rewrite BigN.spec_pred; auto. + generalize Hq; set (a := BigN.to_Z q). + ring_simplify (a - 1 + 1)%Z; auto. + Qed. + |