proposition: Lemma stern_fusc: fusc_prop stern.
proof: Proof. split => //. case => // n. have h := (leq_ltn_trans (leqW (double_le1 n)) (cantor n.*2.+1)). rewrite {1} /stern {1} doubleS sternD_nth_even;apply: (stern_prop h). move => n. move: (leq_ltn_trans (double_le1 n) (ltn_expl n.*2 (ltnSn 1))) => ha. rewrite {1} /stern sternD_nth_odd // -/(stern01 _). by rewrite (stern_prop (ltnW ha)) stern_prop. 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)