proposition: Lemma sternD_rev u v n: sternD v u n = rev (sternD u v n).
proof: Proof. elim:n => //n /= ->; move:(sternD u v n); apply: last_ind => //[] [] // a l x h. have sa: rev (a :: l) != nil by rewrite split_rev. have ww: sternd_rec (rcons (a :: l) x) = rcons (rcons (sternd_rec (a :: l)) ((last 0 (a :: l)) + x)) x. by clear;elim: l a x => // c s Hr a d; rewrite ! rcons_cons - Hr rcons_cons. by rewrite rev_rcons (sternd_rec_aux _ sa) addnC h ww ! rev_rcons head_rev. 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)