proposition: Lemma foldi_lt_l : forall A f from to (a:A), from <? to = true -> foldi f from to a = foldi f (from + 1) to (f from a).
proof: Proof. intros A f from to a Hfromto. pose proof (to_Z_bounded from) as Hfrom. pose proof (to_Z_bounded to) as Hto. unfold foldi. rewrite leb_negb_gtb. rewrite Hfromto; simpl. rewrite ltb_spec in Hfromto. case_eq (to <=? from + 1). rewrite leb_spec, to_Z_add_1_wB; [ | lia ]. intro Htofrom. assert (H : to = from + 1). rewrite <- to_Z_eq. rewrite to_Z_add_1_wB; lia. rewrite H; clear H. replace (from + 1 - from) with 1 by ring. rewrite iter_int63_S; [ | reflexivity ]. change (1 - 1) with 0. reflexivity. replace (to - (from + 1)) with (to - from - 1) by ring. rewrite iter_int63_S. rewrite (iter_int63_comm _ _ (fun jy : int * A => let (j, y) := jy in (j + 1, f j y)) (from, a)). reflexivity. rewrite ltb_spec, to_Z_0, sub_spec, Zmod_small; lia. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz