proposition: Lemma nth_stern11_sym n i: i <= 2 ^n -> nth 0 (stern11 n) i = stern (2^n.+1 - i).
proof: Proof. move => H;rewrite -stern11_symmetric nth_rev size_sternD ?ltnS // subnS subSKn. by rewrite nth_stern11 ? leq_subr// addnBA // addnn expn2S. 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)