diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-18 08:39:19 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-18 08:39:19 -0400 |
| commit | f8d72ab7f44ed944156bb969990f99bd93410a17 (patch) | |
| tree | 99aec2bd6d3e46e847a47b96d569de8c02488367 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
| parent | c7123e2a55c2751e83518c0866baac254f51ec3d (diff) | |
rewrote Testbit and factored out some necessary lemmas about 'uniform' bases (bases that are repeats of the same power of 2) into Pow2Base
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index c59e04ca6..7e33ab20f 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -2103,4 +2103,4 @@ Section CanonicalizationProofs. eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption. Qed. -End CanonicalizationProofs. +End CanonicalizationProofs.
\ No newline at end of file |