proposition: Lemma sternD_middle_quo u v k q n (i:= 2^k * (q.*2.+1)) (S := sternD u v n): i < 2^n -> nth 0 S i.-1 + nth 0 S i.+1 = (k.*2.+1) * (nth 0 S i).
proof: Proof. rewrite /i /S; clear => h. have ha: k < n. by rewrite -(ltn_exp2l k n (ltnSn 1));apply: leq_ltn_trans h;apply:leq_pmulr. move: h. rewrite - (subnK ha); set m := _ - _; rewrite -addSnnS. rewrite addnC expnD ltn_pmul2l ? expn_gt0 // -doubleS expn2S leq_double => h. clear ha;move: m h; elim: k q => [q m lqm | k Hrec q m lqm]. by rewrite add0n !mul1n - doubleS !sternD_nth_even sternD_nth_odd. set i := (2 ^ k * q.*2.+1). have ha: i< 2 ^ (k + m.+1). by rewrite /i expnD ltn_pmul2l ? expn_gt0 // -doubleS expn2S leq_double. have hb:= (leq_ltn_trans (leq_pred i) ha). have ip: 0 < i by rewrite muln_gt0 expn_gt0. have eq1: i.*2.-1 = (i.-1).*2.+1 by rewrite -{1} (prednK ip) doubleS. rewrite addSn expn2S - doubleMl sternD_nth_even sternD_nth_odd // eq1. rewrite sternD_nth_odd // (prednK ip) (addnC (nth _ _ i)) addnACA. by rewrite Hrec // addnA - mulSnr - mulSnr doubleS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)