proposition: Lemma foldi_lt_r : forall A f from to (a:A), from <? to = true -> foldi f from to a = f (to - 1) (foldi f from (to - 1) a).
proof: Proof. intros A f from to a; rewrite ltb_spec; intro Hlt. assert (Bfrom := to_Z_bounded from); assert (Bto := to_Z_bounded to). replace from with (max_int - (max_int - from)) by ring. revert a; pattern (max_int - from). apply (int_ind_bounded _ (max_int - (to - 1))). rewrite leb_spec, sub_spec, to_Z_sub_1_0, sub_spec, max_int_wB, 2!Z.mod_small by lia; lia. intro a; replace (max_int - (max_int - (to - 1))) with (to - 1) by ring. rewrite foldi_lt_l by (rewrite ltb_spec, to_Z_sub_1_0; lia). ring_simplify (to - 1 + 1). rewrite 2!foldi_ge by (rewrite leb_spec; lia); reflexivity. intro i; rewrite leb_spec, ltb_spec, sub_spec, to_Z_sub_1_0, sub_spec, max_int_wB, 2!Z.mod_small by lia. intros Hi1 Hi2 IH a. rewrite foldi_lt_l by (rewrite ltb_spec, sub_spec, to_Z_add_1_wB, max_int_wB, Z.mod_small by lia; lia). rewrite (foldi_lt_l _ _ (max_int - (i + 1))) by (rewrite ltb_spec, sub_spec, to_Z_add_1_wB, to_Z_sub_1_0, max_int_wB, Z.mod_small by lia; lia). replace (max_int - (i + 1) + 1) with (max_int - i) by ring. apply IH. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz