diff options
Diffstat (limited to 'src/NewBaseSystem.v')
-rw-r--r-- | src/NewBaseSystem.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/NewBaseSystem.v b/src/NewBaseSystem.v index 6f1ac11e3..ab115adad 100644 --- a/src/NewBaseSystem.v +++ b/src/NewBaseSystem.v @@ -391,9 +391,11 @@ Module B. Lemma reduction_rule a b s c m (m_eq:Z.pos m = s - c): (a + s * b) mod m = (a + c * b) mod m. Proof. - rewrite m_eq. assert (Z.pos m <> 0) by (intro; discriminate). clear m_eq. - replace (a + s * b) with ((a + c*b) + b*(s-c)) by nsatz. - rewrite Z.add_mod, Z_mod_mult, Z.add_0_r, Z.mod_mod; trivial. Admitted. + rewrite m_eq. pose proof (Pos2Z.is_pos m). + replace (a + s * b) with ((a + c*b) + b*(s-c)) by ring. + rewrite Z.add_mod, Z_mod_mult, Z.add_0_r, Z.mod_mod by omega. + trivial. + Qed. Lemma eval_reduce s c p (s_nonzero:s<>0) m (m_eq : Z.pos m = s - eval c) : mod_eq m (eval (reduce s c p)) (eval p). Proof. |