Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleaning up freeze-related organization and definitions along the way

1 files changed, 8 insertions, 0 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v
index a12d88f9c..16699b8a2 100644
--- a/src/ModularArithmetic/ModularBaseSystemListProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v
@@ -116,6 +116,14 @@ Section LengthProofs.
     rewrite map2_length, map_length, length_modulus_digits.
     apply Min.min_case; omega.
   Qed.
+  Hint Rewrite @length_conditional_subtract_modulus : distr_length.
+  
+  Lemma length_freeze {u} :
+    length u = length limb_widths
+    -> length (freeze u) = length limb_widths.
+  Proof.
+    intros; unfold freeze; repeat autorewrite with distr_length; congruence.
+  Qed.
 
   Lemma length_pack : forall {target_widths}
                              {target_widths_nonneg : forall x, In x target_widths -> 0 <= x}