diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-12-01 10:00:05 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-12-01 10:00:05 +0100 |
| commit | 442e82e6ffc6958192f73382d2270e926ead9c80 (patch) | |
| tree | 24409429d6ab33acaa16d30bac07558d5204b7aa /lib/Integers.v | |
| parent | d4070c456e71b6edfc9b65e5ec837370fea8e9d0 (diff) | |
| download | compcert-kvx-442e82e6ffc6958192f73382d2270e926ead9c80.tar.gz compcert-kvx-442e82e6ffc6958192f73382d2270e926ead9c80.zip | |
Added simple div_one Theorem variants.
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 6 |
1 files changed, 6 insertions, 0 deletions
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. |