FinMatrix.CoqExt.RExt.RExtPow

Require Export RExtBase RExtSqr.

Hint Rewrite
  pow1
  pow_O
  pow_1
  : R.

Convert `a ^ (n + 2)` to `(a ^ 2) * (a ^ n)`

Ltac simp_pow :=
  try match goal with
    | |- context[?a ^ 4] => replace (a ^ 4) with ((a ^ 2) ^ 2); [|ring]
    | |- context[?a ^ 3] => replace (a ^ 3) with ((a ^ 2) * a)%R; [|ring]
    end;
  try rewrite !Rpow2_Rsqr in *.