From 5d201faea9746aca41aeb98361037cf54d5170eb Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 27 Sep 2023 17:00:39 +0200 Subject: [PATCH] Compatible with MathComp dev (2.1) --- theories/hanson.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/hanson.v b/theories/hanson.v index af6c441..b8ca823 100644 --- a/theories/hanson.v +++ b/theories/hanson.v @@ -540,7 +540,7 @@ suff [K [Kpos KP]] : exists K : rat, suff: (C n m.+1)%:R <= (k%:Q + 1) * 3%:R ^ n. by rewrite -[_ + 1%:R]natrD -[_ ^ n]natrX -natrM ler_nat addn1. exact/le_trans/ler_wpM2r/ltW/leKSn/exprz_ge0. -move mE: 10%:Q => m. +move mE: 10%N%:Q => m. (* FIXME *) have lt0m : 0 < m by rewrite -mE. have le0m : 0 <= m by exact: ltW. have lt1m : 1 < m by rewrite -mE.