example

thery · Oct 12, 2024 · a5126e9 · a5126e9
1 parent 784a16f
commit a5126e9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/euler.v b/euler.v
@@ -19,7 +19,7 @@ Qed.
 
 Definition res_quad p a := has (fun i => (i * i) %% p == a) (iota 0 p).
 
-Compute res_quad 4 2.
+Compute res_quad 7 4.
 
 Lemma res_quadP a p : 
   reflect (exists i : 'I_p, (i * i) %% p = a) (res_quad p a).