fact: Definition binary_power_mult (mul : list Z -> list Z -> list Z) : list Z -> list Z -> positive -> list Z := fix f (x a : list Z) (p : positive) : list Z := match p with | xH => mul a x | xO q => f (mul x x) a q | xI q => f (mul x x) (mul a x) q end.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)