# --- T2-COPYRIGHT-BEGIN ---
# t2/package/*/compcert/pos-iter-same.patch
# Copyright (C) 2025 The T2 SDE Project
# SPDX-License-Identifier: GPL-2.0 or patched project license
# --- T2-COPYRIGHT-END ---

--- CompCert-3.15/flocq/IEEE754/BinarySingleNaN.v.vanilla	2024-12-13 11:06:04.000000000 +0100
+++ CompCert-3.15/flocq/IEEE754/BinarySingleNaN.v	2025-07-21 18:03:11.059975056 +0200
@@ -1582,6 +1582,15 @@
 
 (** Normalization and rounding *)
 
+Lemma iter_same : forall A : Type,
+                  forall f : A -> A,
+                  forall x : A,
+                  forall n : positive,
+                  BinPos.Pos.iter f x n = PosDef.Pos.iter f x n.
+intros A f x n.
+induction n; simpl; reflexivity.
+Qed.
+
 Theorem shl_align_correct':
   forall mx ex e,
   (e <= ex)%Z ->
@@ -1595,7 +1604,11 @@
 - now replace ex with ex' by lia.
 - exfalso ; lia.
 - refine (conj _ eq_refl).
-  rewrite shift_pos_correct, Zmult_comm.
+  pose proof (shift_pos_correct d mx) as Aux0.
+  unfold shift_pos in Aux0.
+  pose proof (f_equal Z.pos (iter_same _ xO mx d)) as Aux1.
+  pose proof (eq_trans (eq_sym Aux1) Aux0) as shift_pos_correct'.
+  rewrite shift_pos_correct', Zmult_comm.
   change (Zpower_pos 2 d) with (Zpower radix2 (Z.opp (Z.neg d))).
   rewrite <- Hd.
   replace (- (ex' - ex))%Z with (ex - ex')%Z by ring.