From 95b1c2845527085e8da82b2deae2b80517f34962 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 21 Oct 2024 14:14:42 +0200 Subject: [PATCH] adapt to coq#19611 --- classical/functions.v | 2 +- classical/mathcomp_extra.v | 2 +- theories/exp.v | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/classical/functions.v b/classical/functions.v index cab1dbc50..e40e2819c 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -1253,7 +1253,7 @@ Lemma odflt_unbind : odflt x = unbind (fun=> x) idfun. Proof. by []. Qed. HB.instance Definition _ := Inv.Build _ _ (odflt x) some. HB.instance Definition _ := SplitBij.copy (odflt x) - [the {bij some @` A >-> A} of unbind (fun=> x) idfun]. + [the {splitbij some @` A >-> A} of @unbind (option T) T (fun=> x) idfun]. End Odflt. diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 4e1150553..9fa2fa0a9 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -40,7 +40,7 @@ Lemma ler_sqrt {R : rcfType} (a b : R) : (0 <= b -> (Num.sqrt a <= Num.sqrt b) = (a <= b))%R. Proof. have [b_gt0 _|//|<- _] := ltgtP; last first. - by rewrite sqrtr0 -sqrtr_eq0 le_eqVlt ltNge sqrtr_ge0 orbF. + by rewrite sqrtr0 -[RHS]sqrtr_eq0 le_eqVlt ltNge sqrtr_ge0 orbF. have [a_le0|a_gt0] := ler0P a; last by rewrite ler_psqrt// ?qualifE/= ?ltW. by rewrite ler0_sqrtr // sqrtr_ge0 (le_trans a_le0) ?ltW. Qed. diff --git a/theories/exp.v b/theories/exp.v index 5488a9c91..2e2d30497 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -974,7 +974,7 @@ have ap0 : (0 < a `^ p)%R by rewrite powR_gt0. have bq0 : (0 < b `^ q)%R by rewrite powR_gt0. have := @concave_ln _ (@Itv.mk _ `[0, 1] _ q01)%R _ _ ap0 bq0. have pq' : (p^-1 = 1 - q^-1)%R by rewrite -pq addrK. -rewrite !convRE/= /onem -pq' -ler_expR expRD (mulrC p^-1). +rewrite !convRE/= /onem -pq' -[_ <= ln _]ler_expR expRD (mulrC p^-1). rewrite ln_powR mulrAC divff ?mul1r ?gt_eqF// (mulrC q^-1). rewrite ln_powR mulrAC divff ?mul1r ?gt_eqF//. rewrite lnK ?posrE// lnK ?posrE// => /le_trans; apply.