diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-06-18 15:13:49 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-06-18 15:13:49 -0400 |
| commit | 3b87c0b0b45d8c7982624d1cf71e29d3ceb8eb2f (patch) | |
| tree | c8e73a097b7ecfe369bd0464176bc74358bb1c9b /src/Arithmetic/Saturated.v | |
| parent | f35223a09bb224cca7f7a978c9286c340ffe0c66 (diff) | |
proved small_zero
Diffstat (limited to 'src/Arithmetic/Saturated.v')
| -rw-r--r-- | src/Arithmetic/Saturated.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index 17c7bc057..747c34501 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -805,6 +805,13 @@ Section API. reflexivity. Qed. + Lemma small_zero n : small (@zero n). + Proof. + cbv [zero small B.Positional.zeros]. destruct n; [simpl;tauto|]. + rewrite to_list_repeat. + intros x H; apply repeat_spec in H; subst x; omega. + Qed. + Lemma eval_join0 n p : eval (@join0 n p) = eval p. Proof. |