proposition: Lemma stern_gt0 k: (0 < stern k) = (0 < k).
proof: Proof. case: k => // k. have-> : stern k.+1 = nth 1 (stern01 k.+1) k.+1. apply:set_nth_default; rewrite size_sternD ltnS ltnW //; apply:cantor. by rewrite (sternD_01_positive) lt0n. 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)