proposition: Lemma sternD_sumE u v n : sternD_sum u v n = ((3^n).+1)./2 * (u + v).
proof: Proof. elim:n u v. by move => a b;rewrite /sternD_sum ! big_cons big_nil addn0 mul1n. rewrite /sternD_sum =>n Hrec a b;apply/eqP. move:(Hrec (a+b) b); rewrite {1} sternD_split1 big_cons addnC => eq1. have o3n: odd (3 ^ n) by elim n => // q hr; rewrite expnS oddM hr. rewrite - (eqn_add2r (a + b)) - mulSnr expnS split_sternD big_cat Hrec - addnA. rewrite eq1 - mulnDr (addnA a) addnn - (addnA a) addnn addnACA. rewrite - mul2n - mulSnr - mul2n - mulSn - mulnDr mulnA (mulnC _ 3). rewrite - [_ ./2.+1]/(((3 * 3^n).+3) ./2) - (addn3 (3 * 3 ^ n)) - mulnSr. rewrite - {2} (odd_double_half ((3 ^ n).+1)) /odd -/odd o3n. by rewrite - muln2 mulnA muln2 doubleK. 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)