fact: Definition fastexp3 {A : Type} (mul : A -> A -> A) (m : A) := fix f (l : list bool) (acc : A) : A := match l with | nil => acc | true :: l => f l (mul (mul acc acc) m) | false :: l => f l (mul acc acc) end.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)