diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-06-11 09:17:09 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-06-11 09:17:09 -0400 |
| commit | a37eb79f7750a419346211abb58ec45b79975da0 (patch) | |
| tree | ba62e0ff6176a8dc208f65bfae52c8415076d107 /src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | |
| parent | 2e566c32baf2a140cd7820c4f06437ee5c43ac44 (diff) | |
starting rewrite using different definition of map
Diffstat (limited to 'src/ModularArithmetic/PseudoMersenneBaseParamProofs.v')
| -rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 1a7b3316e..10bbdf33d 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -89,6 +89,13 @@ Section PseudoMersenneBaseParamProofs. - rewrite IHl by auto; ring. Qed. + Lemma limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. + Proof. + intros. + apply Z.lt_le_incl. + auto using limb_widths_pos. + Qed. + Lemma sum_firstn_limb_widths_nonneg : forall n, 0 <= sum_firstn limb_widths n. Proof. unfold sum_firstn; intros. |