From 3ba79a0e18341806007ec091940eb1b8378ab739 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 6 Mar 2023 17:18:55 +0100 Subject: Upgrade Flocq to 4.1.1 --- flocq/Core/Raux.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'flocq/Core/Raux.v') diff --git a/flocq/Core/Raux.v b/flocq/Core/Raux.v index 4b2ce8d7..432d3214 100644 --- a/flocq/Core/Raux.v +++ b/flocq/Core/Raux.v @@ -214,7 +214,7 @@ destruct (Req_dec x 0) as [Zx|Nzx]. unfold sqrt. destruct Rcase_abs. + reflexivity. - + casetype False. + + exfalso. now apply Nzx, Rle_antisym; [|apply Rge_le]. Qed. @@ -2355,7 +2355,7 @@ assert (H: forall i, (i < N)%nat -> ~ P i). apply archimed. destruct (HP N) as [PN|PN]. now split. -elimtype False. +exfalso. refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _). intros x [y [[Py ->]|[_ ->]]]. destruct (eq_nat_dec y N) as [HyN|HyN]. -- cgit