proposition: Lemma sternD_nth_even u v n k: nth 0 (sternD u v n.+1) (k.*2) = nth 0 (sternD u v n) k.
proof: Proof. rewrite /sternD -/sternD; move: {u v n} (sternD u v n). elim:k; first by case => // a;case. by move => n Hrec [] // a [ | b l ]; rewrite /= ? nth_nil -? (Hrec (b::l)). 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)