proposition: Lemma fastexp3P {A : Type} (op : A -> A -> A) (id e : A) (h l : nat) (v : list bool) (assoc : associative op) (cm : op id e = op e id) (idn : forall a, op id a = a): l = (\sum_(i < size v) nth false v (size v - 1 - i) * 2 ^ i)%N -> iter (h * 2 ^ size v + l) (op e) id = fastexp3 op e v (iter h (op e) id).
proof: Proof. elim: v h l => [| b v Ih] h l. rewrite /= big_ord0 => ->. by rewrite expn0 muln1 addn0. rewrite /= big_ord_recr /=. rewrite -subnDA subnn /=. have body_simp : forall i : 'I_(size v), true -> (nth false (b :: v) ((size v).+1 - 1 - i) * 2 ^ i = nth false v (size v - 1 - i) * 2 ^ i)%N. move=> i _; congr (_ * _)%N. have -> // : ((size v).+1 - 1 - i = ((size v) - 1 - i).+1)%N. case: i =>[i]; case:(size v)=> // n ip /=. by rewrite subSS subn0 -subnDA add1n subSS subSn. rewrite (eq_bigr _ body_simp) {body_simp}. set l' := (l - b * 2 ^ size v)%N. move=> lq. have lq' : l' = (\sum_(i < size v) nth false v (size v - 1 - i) * 2 ^ i)%N. by rewrite /l' lq addnK. have hlq : (h * 2 ^ (size v).+1 + l = (2 * h + b) * 2 ^ (size v) + l')%N. by rewrite expnS mulnA lq addnA addnAC -mulnDl -lq' (mulnC h). rewrite hlq Ih; last by []. clear -assoc cm idn. case: b. congr (fastexp3 op e v). rewrite -!assoc -iter_comm // assoc -iter_comm // -assoc. by rewrite iter_combine // idn -iterS addn1 mulSn mul1n. congr fastexp3. by rewrite iter_combine // idn addn0 mulSn mul1n. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)