diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2015-11-07 14:02:50 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2015-11-07 14:02:50 -0500 |
| commit | 8fd2a0934760ff725052bcb7bdefa6863f006e92 (patch) | |
| tree | 10b77438adb93e8de4bd7b06e9899371ecf047b2 /src/Specific/GF25519.v | |
| parent | b953c040b36f34b480759f0c4cd275eff4d1efa5 (diff) | |
ModularBaseSystem: finish base_good
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 4925f87c5..722b1bde4 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -71,7 +71,7 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb reflexivity. Qed. - Lemma k_pos : 0 <= k. + Lemma k_nonneg : 0 <= k. Proof. rewrite Zle_is_le_bool; reflexivity. Qed. |