proposition: Lemma iter_int63_aux_comm : forall n i A f a, (to_Z i < 2 ^ Z.of_nat n)%Z -> iter_int63_aux n i A f (f a) = f (iter_int63_aux n i A f a).
proof: Proof. intros n i A f; revert i; induction n. intros i a Hi. assert (i = 0). rewrite <- to_Z_eq, to_Z_0. generalize (to_Z_bounded i). change (φ (i) < 1)%Z in Hi. lia. reflexivity. intros i a Hi; simpl. case (i =? 0); [ reflexivity | ]. rewrite IHn; [ | apply pow2_lsr; assumption]. rewrite IHn; [ | apply pow2_lsr; assumption]. case (bit i 0); reflexivity. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz