fact: Fixpoint comp_pow_tree {A} (f : A -> A -> A) (n : nat) (x : A) {struct n} : A := match n with | O => x | S n => f (comp_pow_tree f n x) (comp_pow_tree f n x) end.
imports: Coq.ZArith.ZArith Coq.Setoids.Setoid Coq.Classes.Morphisms