proposition: Lemma foldi_eq_compat : forall A (f1 f2:int -> A -> A) min max a, (forall i a, min <=? i = true -> i <? max = true -> f1 i a = f2 i a) -> foldi f1 min max a = foldi f2 min max a.
proof: Proof. intros A f1 f2 min max a Hf. assert (Bmin := to_Z_bounded min); assert (Bmax := to_Z_bounded max). case (Z.lt_ge_cases [|min|] [|max|]); [ intro Hlt | intro Hle ]. apply (foldi_ind2 _ _ (fun _ a b => a = b)); [ rewrite leb_spec; lia | reflexivity | ]. intros i a1 a2 Hi1 Hi2 Heq; rewrite Heq; apply Hf; assumption. rewrite 2!foldi_ge by (rewrite leb_spec; lia); reflexivity. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz