fact: Fixpoint power `{M: @EMonoid A E_op E_one E_eq} (x:A)(n:nat) := match n with 0%nat => E_one | S p => x * x ^ p end where "x ^ n" := (power x n) : M_scope.
imports: ZArith Div2 Recdef Relations Morphisms Monoid_def Arith Lia