proposition: Lemma sternD_middle_contra u v n i : u != 0 -> v != 0 -> nth 0 (sternD u v n.+1) i = u + v -> i = 2 ^ n.
proof: Proof. move => /negbTE anz /negbTE bnz /eqP; rewrite eq_sym. move:(sternD_at_bounds u v n.+1) => [sa sb]. case kz: (i == 0); first by rewrite (eqP kz) sa -{2} (addn0 u) eqn_add2l bnz. case: (ltngtP i (2^n)) => // kl2. rewrite split_sternD nth_cat size_sternD ltnS (ltnW kl2) => /eqP Hk. have kl3: (0< i < 2^n) by rewrite lt0n kl2 kz. move: (sternD_ge_in_bounds u (u + v) kl3). by rewrite - Hk - {2} (add0n (u + v)) leq_add2r leqn0 anz. case: (ltngtP i (2^n.+1)) => kl1; last first. by rewrite kl1 sb -{2} (add0n v) eqn_add2r anz. by rewrite (nth_default) ?size_sternD // addn_eq0 anz bnz. rewrite split_sternD nth_cat size_sternD ltnS leqNgt kl2 nth_behead => /eqP Hk. move: kl1; rewrite -(subnK kl2) addnS -addSn expnS mul2n -addnn ltn_add2r => lt. have kl3: 0 < (i - (2 ^ n).+1).+1 < 2 ^n by rewrite lt. move: (sternD_ge_in_bounds (u+v) v kl3). by rewrite -Hk - {2} (addn0 (u+v)) leq_add2l leqn0 bnz. 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)