diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-09-21 13:43:52 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-09-21 13:44:10 -0400 |
| commit | 2311b4df116eee1e35465cd225c419c55456899f (patch) | |
| tree | 04ddcf6e5302877c6453bef861e7772fd8dcd557 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
| parent | 3482333812490f41f2bb962fa1c9a48811ec189f (diff) | |
Reorganization, moving of lemmas to correct files, and 8.4 compatibility
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 2deeba0fa..7350fac76 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -823,10 +823,17 @@ Section CanonicalizationProofs. rewrite H1; reflexivity. Qed. + Lemma c_upper_bound : c - 1 < 2 ^ limb_widths[0]. + Proof. + pose proof c_reduce2. pose proof c_pos. + omega. + Qed. + Hint Resolve c_upper_bound. + Lemma minimal_rep_encode : forall x, minimal_rep (encode x). Proof. split; intros; auto using bounded_encode. - apply ge_modulus_spec; auto using length_to_list. + apply ge_modulus_spec; auto using bounded_encode, length_to_list. apply encode_range. Qed. @@ -839,7 +846,7 @@ Section CanonicalizationProofs. apply Fdecode_decode_mod in H. pose proof (Fdecode_decode_mod _ _ (encode_rep x)). rewrite Z.mod_small in H by (apply ge_modulus_spec; distr_length; intuition auto). - rewrite Z.mod_small in H1 by (apply ge_modulus_spec; distr_length; apply minimal_rep_encode). + rewrite Z.mod_small in H1 by (apply ge_modulus_spec; distr_length; auto using c_upper_bound; apply minimal_rep_encode). congruence. Qed. |