proposition: Lemma step1E m n w p : step1 m n w p = step m n w p.
proof: Proof. apply/polyP => i. rewrite coef_poly coef_sum. have [mnLi|iLmn] := leqP. rewrite big1 // => j _; rewrite coef_sum /=. rewrite big1 // => k _; rewrite !coef_poly !(coefD, coefZ, coefXn). rewrite !gtn_eqF ?mulr0 ?addr0 // (leq_trans _ mnLi) //. by apply: bound_step. apply: leq_trans (bound_step (ltn_ord j) (ltn_ord k)). by rewrite ltnS leq_addr. set l := (i %/ 2 ^ n.+1)%N. have l_ltn : (l < 2 ^ m)%N. by rewrite ltn_divLR ?expn_gt0 // -expnD addnS. rewrite (bigD1 (Ordinal l_ltn)) //= [X in _ = _ + X]big1; last first. move=> i1 /eqP/val_eqP /= i1Dl. rewrite coef_sum big1 // => i2 _. rewrite coefD !coefZ !coefXn. case: (ltngtP i1 l) i1Dl => // i1Dl _. rewrite leq_divRL ?expn_gt0 // in i1Dl. rewrite !gtn_eqF ?mulr0 ?addr0 //; apply: leq_trans i1Dl. by rewrite addnAC mulSn -!addSn leq_add // expnS mul2n -addnn leq_add2r. rewrite mulSn -!addSn leq_add // (leq_trans (ltn_ord _)) //. by rewrite expnS mul2n -addnn leq_addr. rewrite ltn_divLR ?expn_gt0 // in i1Dl. rewrite !ltn_eqF ?mulr0 ?addr0 //; apply: leq_trans i1Dl _. by rewrite addnAC leq_addl. by rewrite leq_addl. rewrite addr0. have F : (i %% 2 ^ n.+1 + l * 2 ^ n.+1 = i)%N by rewrite addnC -divn_eq. rewrite coef_sum. case: leqP => H. have Fi : (2 ^ n <= i)%N by apply: leq_trans H (leq_mod _ _). have F1 : (i %% 2 ^ n.+1 - 2 ^ n < 2 ^ n)%N. by rewrite ltn_subLR // addnn -mul2n -expnS ltn_pmod ?expn_gt0. have F2 : ((i %% 2 ^ n.+1) %% 2 ^ n = i %% 2 ^ n.+1 - 2 ^ n)%N. by rewrite -[in LHS](subnK H) modnDr modn_small. rewrite (bigD1 (Ordinal F1)) //= ?big1. rewrite addr0 coefD !coefZ !coefXn. rewrite addnBAC // F subnK // eqxx mulr1 gtn_eqF; last first. by rewrite ltn_subLR // (ltn_add2r _ 0) expn_gt0. rewrite mulr0 add0r !coef_poly F1. by rewrite addnBAC // F subnK // eqxx mulr1 gtn_eqF. move=> i1 /eqP/val_eqP/= Hi1. rewrite !coef_poly ltn_ord coefD !coefZ !coefXn. rewrite -F addnAC !eqn_add2r gtn_eqF ?mulr0 ?add0r; last first. by apply: leq_trans H. by rewrite -(subnK H) eqn_add2r eq_sym (negPf Hi1) mulr0. rewrite (bigD1 (Ordinal H)) //= ?big1. rewrite addr0 coefD !coefZ !coefXn F. rewrite eqxx mulr1 ltn_eqF ?mulr0 ?addr0 // ?(ltn_add2l _ 0) ?expn_gt0 //. by rewrite !coef_poly F H. by rewrite addnC (ltn_add2r _ 0) expn_gt0. move=> i1 /eqP/val_eqP/= Hi1. rewrite !coef_poly ltn_ord coefD !coefZ !coefXn. rewrite -F eqn_add2r eq_sym (negPf Hi1) mulr0 add0r. rewrite addnAC eqn_add2r ltn_eqF ?mulr0 //. by apply: leq_trans H (leq_addl _ _). Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn