proposition: Lemma afold_right_spec : forall A args op (e : A), (forall a, op a e = a) -> afold_right _ e op args = foldi (fun i a => op (args.[length args - 1 - i]) a) 0 (length args) e.
proof: Proof. unfold afold_right;intros A args op neu H10. assert (Bargs := to_Z_bounded (length args)). destruct (reflect_eqb (length args) 0) as [e|n]. rewrite e, foldi_ge by reflexivity;trivial. change 1 with (0 + 1) at 2. replace (length args - 1) with (length args - 1 - 0) at 1 by ring. rewrite <- (H10 (args.[length args - 1 - 0])). rewrite <- (foldi_lt_l _ (fun i => op (args.[length args - 1 - i]))) by (apply not_0_ltb; assumption). apply foldi_eq_compat; intros; reflexivity. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz