proposition: Lemma sternD_01_positive n i: 0 < nth 1 (sternD 0 1 n) i.+1.
proof: Proof. elim:n i; first by case => //; case. move => n; rewrite/sternD -/(sternD); elim:(sternD 0 1 n) => // a. case => // b l Hrec aux; have bp := (aux 0). case; [by rewrite /= addn_gt0 bp orbT | case; [ by case l | move => k]]. apply: Hrec => j; exact: (aux j.+1). 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)