1 files changed, 3 insertions, 3 deletions
diff --git a/src/ModularArithmetic/PseudoMersenneBaseRep.v b/src/ModularArithmetic/PseudoMersenneBaseRep.v
index c16cc8d38..6b4d29a35 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseRep.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseRep.v
@@ -25,7 +25,7 @@ Class RepZMod (modulus : Z) := {
 
 Class SubtractionCoefficient (m : Z) (prm : PseudoMersenneBaseParams m) := {
   coeff : BaseSystem.digits;
-  coeff_length : (length coeff <= length PseudoMersenneBaseParamProofs.base)%nat;
+  coeff_length : (length coeff = length PseudoMersenneBaseParamProofs.base)%nat;
   coeff_mod: (BaseSystem.decode PseudoMersenneBaseParamProofs.base coeff) mod m = 0
 }.
 
@@ -45,6 +45,6 @@ Instance PseudoMersenneBase m (prm : PseudoMersenneBaseParams m) (sc : Subtracti
   sub := ModularBaseSystem.sub coeff coeff_mod;
   sub_rep := ModularBaseSystemProofs.sub_rep coeff coeff_mod coeff_length;
 
-  mul := ModularBaseSystem.mul;
-  mul_rep := ModularBaseSystemProofs.mul_rep
+  mul := ModularBaseSystem.carry_mul;
+  mul_rep := ModularBaseSystemProofs.carry_mul_rep
 }.