From c00de4298c66965885e6ade605f8a2924f89a321 Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 2 Mar 2017 14:05:38 -0500 Subject: Fixed admit left from fsatz port --- src/NewBaseSystem.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'src/NewBaseSystem.v') 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. -- cgit v1.2.3