proposition: Lemma afold_left_spec : forall A args op (e : A), (forall a, op e a = a) -> afold_left _ e op args = foldi (fun i a => op a (args.[i])) 0 (length args) e.
proof: Proof. unfold afold_left;intros A args op neu H10. destruct (reflect_eqb (length args) 0) as [e|n]. rewrite e, foldi_ge by reflexivity;trivial. rewrite (foldi_lt_l _ _ 0) by (apply not_0_ltb; assumption). f_equal; rewrite H10; reflexivity. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz