odd_div_upi_not_half

IBM · May 22, 2024 · 953992e · 953992e
1 parent 7e149e5
commit 953992e
Showing 1 changed file with 6 additions and 5 deletions.
diff --git a/coq/FHE/arith.v b/coq/FHE/arith.v
@@ -2611,13 +2611,14 @@ Proof.
   {
     exists ((upi (c%:~R / p%:~R)%R)*+p - c).
     rewrite -H0.
-    rewrite rmorphD rmorphN /= mulrnDl.
-    f_equal.
-    - ring.
-    - admit.
+    field.
+    replace (zero (Ring.zmodType (ssrnum.Num.NumField.ringType R_numFieldType)))
+      with (((0%:R):R)) by lra.
+    rewrite eqr_nat.
+    lia.
   }
   by generalize (odd_mul_half p H); intros.
-Admitted.
+Qed.
 
 Lemma odd_div_upi_compare (p : nat) (c : int) :
   odd p ->