proposition: Lemma Stern_consecutive_nn a : Stern_consecutive a a -> a = 1.
proof: Proof. move => [n [i []]]. case:n => [| n lta]; first by rewrite ltnS leqn0 => /eqP -> /=. have hb: i./2 < 2 ^ n. rewrite -ltn_double -expn2S; exact: (leq_ltn_trans (double_half_le i) lta). have hc:=(sternD_nth_compare_strict (ltnSn 0)(ltnSn 0) hb). case (odd_dichot i) => ea hd he; move: hc; rewrite - ea hd he gtn_max ltnn ? andbF //. 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)