proposition: Lemma binary_correct : forall p x, computation_eval (bin_pow_scheme p (A:=A) x) == x ^ (Pos.to_nat p).
proof: Proof. intros p ; induction p. - simpl. intro a. unfold computation_eval in *; simpl. rewrite <- computation_eval_rw. rewrite axp_correct. replace (Pos.iter_op Init.Nat.add p 2%nat) with (Pos.to_nat p + Pos.to_nat p)%nat. destruct M;rewrite power_of_plus; auto. f_equal. now rewrite <- power_of_square. now rewrite ZL6. - simpl. intro a. unfold computation_eval in *; simpl; rewrite IHp; unfold mult_op. generalize (sqr_eqn M a); unfold mult_op. intro H; generalize (power_proper M); intro H0; rewrite Pos2Nat.inj_xO. transitivity ((a^2) ^ Pos.to_nat p). apply H0. red in H. destruct M; destruct Eq_equiv. symmetry;auto. reflexivity. rewrite (power_of_power M). now rewrite Nat.mul_comm. - simpl. intros; now monoid_simpl M. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)