From 442e82e6ffc6958192f73382d2270e926ead9c80 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 1 Dec 2017 10:00:05 +0100
Subject: Added simple div_one Theorem variants.

---
 lib/Integers.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'lib/Integers.v')

diff --git a/lib/Integers.v b/lib/Integers.v
index b849872f..7fb29803 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -1178,6 +1178,12 @@ Proof.
   unfold divu; intros. rewrite unsigned_one. rewrite Zdiv_1_r. apply repr_unsigned.
 Qed.
 
+Theorem divs_one:
+  forall x, zwordsize > 1 -> divs x one = x.
+Proof.
+  unfold divs; intros. rewrite signed_one. rewrite Zquot_1_r. apply repr_signed. auto.
+Qed.
+
 Theorem modu_one:
   forall x, modu x one = zero.
 Proof.
-- 
cgit