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