proposition: Lemma foldi_ind2 : forall A B (P : int -> A -> B -> Prop) f1 f2 from to a1 a2, from <=? to = true -> P from a1 a2 -> (forall i a1 a2, from <=? i = true -> i <? to = true -> P i a1 a2 -> P (i + 1) (f1 i a1) (f2 i a2)) -> P to (foldi f1 from to a1) (foldi f2 from to a2).
proof: Proof. intros A B P f1 f2 from to a1 a2 Hle Hfrom IH. assert (Bfrom := to_Z_bounded from); assert (Bto := to_Z_bounded to). pattern to; apply (int_ind_bounded _ from). exact Hle. rewrite 2!foldi_ge by (rewrite leb_spec; lia). exact Hfrom. intro i; assert (Bi := to_Z_bounded i). rewrite leb_spec, ltb_spec; intros Hi1 Hi2; rewrite 2!(foldi_lt_r _ _ _ (i + 1)) by (rewrite ltb_spec, to_Z_add_1_wB; lia). ring_simplify (i + 1 - 1); apply IH; [ rewrite leb_spec; exact Hi1 | rewrite ltb_spec; exact Hi2 ]. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz