fact: Fixpoint group_power_pos (g : G) (p : positive) {struct p} : G := match p with | xH => g | xO p' => group_square (group_power_pos g p') | xI p' => sgroup_law G (group_square (group_power_pos g p')) g end.
imports: Zring