proposition: Lemma iter_int63_S : forall i A f a, 0 <? i = true -> iter_int63 i A f a = f (iter_int63 (i - 1) A f a).
proof: Proof. intros i A f a. rewrite ltb_spec, to_Z_0; intro Hi. unfold iter_int63. apply iter_int63_aux_S. split; [ lia | ]. apply pow2_size. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz