aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega/OmegaLemmas.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/omega/OmegaLemmas.v')
-rw-r--r--plugins/omega/OmegaLemmas.v7
1 files changed, 7 insertions, 0 deletions
diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v
index ff433bbd8..5b6f4670f 100644
--- a/plugins/omega/OmegaLemmas.v
+++ b/plugins/omega/OmegaLemmas.v
@@ -298,3 +298,10 @@ Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop)
Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop)
(H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x).
+
+Theorem intro_Z :
+ forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
+Proof.
+ intros n; exists (Z_of_nat n); split; trivial.
+ rewrite Zmult_1_r, Zplus_0_r. apply Zle_0_nat.
+Qed.