proposition: Lemma afold_left_eq : forall A OP (def : A) V1 V2, length V1 = length V2 -> (forall i, i <? length V1 = true -> V1.[i] = V2.[i]) -> afold_left _ def OP V1 = afold_left _ def OP V2.
proof: Proof. intros A OP def V1 V2 Heqlength HeqV. assert (BV1 := to_Z_bounded (length V1)). unfold afold_left. rewrite <- Heqlength. case (reflect_eqb (length V1) 0). reflexivity. rewrite <- to_Z_eq, to_Z_0; intro Hneq. rewrite <- HeqV by (rewrite ltb_spec, to_Z_0; lia). apply (foldi_ind2 _ _ (fun i a b => a = b)). rewrite leb_spec, to_Z_1; lia. reflexivity. intros i a1 a2; assert (Bi := to_Z_bounded i). rewrite leb_spec, to_Z_1; intro Hi1. rewrite ltb_spec by lia; intros Hi2 IH. f_equal;[ exact IH | apply HeqV; rewrite ltb_spec; lia ]. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz