proposition: Lemma axp_correct : forall p a x, computation_eval (axp_scheme p a x) == a * x ^ (Pos.to_nat p).
proof: Proof. induction p. - intros a x; simpl axp_scheme. replace (Pos.to_nat p~1) with (S (Pos.to_nat p + Pos.to_nat p)%nat). cbn. rewrite <- computation_eval_rw, IHp. unfold equiv in *. destruct M; rewrite power_of_square, power_of_plus. unfold mult_op in *; repeat rewrite Eop_assoc. destruct Eq_equiv. reflexivity. rewrite Pnat.Pos2Nat.inj_xI;lia. - intros a x; simpl axp_scheme. replace (Pos.to_nat p~0 ) with (Pos.to_nat p + Pos.to_nat p)%nat. unfold computation_eval in *. destruct M; simpl; rewrite IHp, power_of_square, <- power_of_plus. reflexivity. rewrite Pnat.Pos2Nat.inj_xO;lia. - simpl; destruct M; intros; now rewrite (Eone_right x). Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)