proposition: Lemma binary_power_mult_ok : forall p a x, binary_power_mult x a p == a * x ^ Pos.to_nat p.
proof: Proof. induction p as [q IHq | q IHq|]. - intros; cbn. rewrite Pos2Nat.inj_xI, IHq. rewrite power_eq2, Eop_assoc. rewrite <- power_of_power, sqr_eqn, power_of_square; reflexivity. - intros; cbn. rewrite Pos2Nat.inj_xO, IHq. rewrite <- power_of_power, sqr_eqn, power_of_square; reflexivity. - intros; cbn. simpl (x ^ Pos.to_nat 1). now monoid_rw. Qed.
imports: ZArith Div2 Recdef Relations Morphisms Monoid_def Arith Lia