From f434c4bcf99f10e1a38c34084a93984dba787c64 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sat, 13 Jul 2024 10:06:26 +0200 Subject: [PATCH] tweaks --- robust/weightedmean.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/robust/weightedmean.v b/robust/weightedmean.v index 76d05010..4338d8a0 100644 --- a/robust/weightedmean.v +++ b/robust/weightedmean.v @@ -468,8 +468,8 @@ Qed. End pos_evar. -Notation eps_max := (10 / 127)%mcR. -Notation denom := (335 / 100)%mcR. +Notation eps_max := (10 / 126)%mcR. +Notation denom := ((3 / 10)^-1)%mcR. Section invariant. Local Open Scope ring_scope.