fact: Fixpoint binary_power_mult `{M: @EMonoid A E_op E_one E_eq} (x a:A)(p:positive) : A := match p with | xH => a * x | xO q => binary_power_mult (x * x) a q | xI q => binary_power_mult (x * x) (a * x) q end.
imports: ZArith Div2 Recdef Relations Morphisms Monoid_def Arith Lia