proposition: Lemma reverse_polyS n p : reverse_poly n.+1 p = reverse_poly n (even_poly p) + reverse_poly n (odd_poly p) * 'X^(2 ^ n).
proof: Proof. rewrite /reverse_poly /even_poly /odd_poly. under [X in X + _]eq_poly do rewrite coef_poly. under [X in _ + X * _]eq_poly do rewrite coef_poly. apply/polyP => i. rewrite coefD coefMXn !coef_poly. have [tnLi|iLtn] := leqP (2 ^ n) i. rewrite ltn_subLR // addnn -mul2n -expnS add0r. case: leqP => [//|iLtSn]. suff Hf : (rdigitn 2 n.+1 i) = (rdigitn 2 n (i - 2 ^ n)).*2.+1. case: leqP => [iLn|nLi]; last by rewrite Hf. suff/leq_sizeP-> : (size p <= rdigitn 2 n.+1 i)%N by []. rewrite Hf. by rewrite leq_half_double in iLn. rewrite !rdigitnE big_ord_recl /= subn0 muln1 /bump /= . rewrite {1}/digitn -{1}(subnK tnLi). rewrite divnDr ?dvdnn // divnn expn_gt0 /= divn_small ?add1n; last first. by rewrite ltn_subLR // addnn -mul2n -expnS. under eq_bigr do rewrite add1n; congr (_.+1). under eq_bigr do rewrite expnS mulnCA. rewrite -big_distrr /= mul2n; congr (_.*2). apply: eq_bigr => j _; congr (_ * _)%N. have ->: (n.-1 - j = n - j.+1)%N. rewrite subnS. by case: (n) j => //= n1 j; rewrite subSn // -ltnS. rewrite /digitn -{1}(subnK tnLi) -[X in (_ + 2 ^ X)%N](subnK (ltn_ord j)). rewrite expnD mulnC divnDMl ?expn_gt0 //. by rewrite -modnDm // expnS modnMr addn0 modn_mod. rewrite addr0 ifT; last by rewrite (leq_trans iLtn) // leq_exp2l. suff Hf : (rdigitn 2 n.+1 i) = (rdigitn 2 n i).*2. case: leqP => [iLn|nLi]; last by rewrite Hf. suff/leq_sizeP-> : (size p <= rdigitn 2 n.+1 i)%N by []. rewrite leq_uphalf_double in iLn. by rewrite (leq_trans iLn) // Hf. rewrite !rdigitnE big_ord_recl /= subn0 muln1 /bump /= . rewrite {1}/digitn divn_small // add0n. under eq_bigr do rewrite add1n expnS mulnCA. rewrite -big_distrr /= mul2n; congr (_.*2). apply: eq_bigr => j _; congr (_ _ _ * _)%N. rewrite subnS. by case: (n) j => //= n1 j; rewrite subSn // -ltnS. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn