fact: Fixpoint fastexp (m : list Z) (p : positive) : list Z := match p with | xH => m | xI p => let r := fastexp m p in m3lmul (m3lmul r r) m | xO p => let r := fastexp m p in m3lmul r r end.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)