proposition: Lemma split_sternD u v n : (sternD u v n.+1) = (sternD u (u + v) n) ++- (sternD (u + v) v n).
proof: Proof. elim:n => // n /= ->. rewrite (sternD_split1 (u+v) v n) (sternD_split2 u (u+v) n) [LHS]/=. set A := belast _ _; set B := behead _; elim: A (u+v); first by case:B. move => a l Hr b. have ha: rcons l b != [::] by case l. have hc: rcons l b ++ B != [::] by case l. have hb: head 0 (rcons l b ++ B) = head 0 (rcons l b) by case l. by rewrite rcons_cons cat_cons (sternd_rec_aux _ hc)(sternd_rec_aux _ ha) Hr hb. 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)