From 7f7994448c57b8ee28d578ce9f26d34202f2231c Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 2 Aug 2024 10:21:18 +0200 Subject: [PATCH] fix --- refinements/binord.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/refinements/binord.v b/refinements/binord.v index ffee146..2fd0d6e 100644 --- a/refinements/binord.v +++ b/refinements/binord.v @@ -118,7 +118,7 @@ Local Arguments mul_ord /. #[export] Instance Rord_mul n1 n2 (rn : nat_R n1 n2) : refines (Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn) ==> Rord (nat_R_S_R rn)) - (@Zp_mul n1.+1) *%C. + (@Zp_mul _) *%C. Proof. rewrite refinesE=> x x' hx y y' hy /=. exact: refinesP.