proposition: Lemma stern_prop i j: i <= 2^j -> nth 0 (stern01 j) i = stern i.
proof: Proof. have rec k n: k <= 2^n -> nth 0 (stern01 n.+1) k = nth 0 (stern01 n) k. by move => h; rewrite - (split_stern01_left n);rewrite nth_take //. move => le1; case /orP: (leq_total i j) => le2. rewrite -(subnK le2); elim:(j-i) => // k Hrec; rewrite addSn rec //. by apply: leq_trans (ltnW (cantor (k+i))); rewrite leq_addl. rewrite /stern -{2} (subnK le2); elim: (i -j) => // k Hrec. by rewrite addSn rec ? Hrec // (leq_trans le1) // leq_exp2l //leq_addl. 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)