proposition: Lemma power_mult_correct : forall n x, tail_recursive_power x n = x ** n.
proof: Proof. intros n x; unfold tail_recursive_power. rewrite <- (one_left (power x n)). assert (forall y:A, power_mult y x n = y * (power x n)); auto. generalize n x;intro p; induction p;simpl;intros; monoid_simpl;auto. Qed.
imports: ZArith Recdef Mat Ring