proposition: Lemma Stern_pair_injective i n j m: i < 2^n -> j < 2^m -> nth 0 (stern11 n) i = nth 0 (stern11 m) j -> nth 0 (stern11 n) i.+1 = nth 0 (stern11 m) j.+1 -> i = j /\ n = m.
proof: Proof. move => ha hb; move: (ltnW ha) (ltnW hb) => hc hd. rewrite ! nth_stern11 // !addnS => sa sb. suff sc: (2 ^ n + i) = (2 ^ m + j). have he: 2^n +i < 2^n.+1 by rewrite expn2S -addnn ltn_add2l. have hf: 2^m +j < 2^m.+1 by rewrite expn2S -addnn ltn_add2l. case: (ltngtP n m). + rewrite - (leq_exp2l _ _ (ltnSn 1)) => xx. by move:(leq_trans he xx); rewrite sc ltnNge leq_addr. + rewrite - (leq_exp2l _ _ (ltnSn 1)) => xx. by move:(leq_trans hf xx); rewrite - sc ltnNge leq_addr. + by move => ea; move/eqP:sc; rewrite ea eqn_add2l => /eqP ->. move: sa sb; move: (2 ^ n + i) (2 ^ m + j); clear => n m. wlog : n m / n <= m. move => Hrec sa sb; case /orP:(leq_total n m) => sc; first by apply: Hrec. symmetry; apply: Hrec => //. have aux a b c: b +a + c = a -> (b==0) && (c == 0). by rewrite (addnC b) -addnA -{2} (addn0 a) - addn_eq0 - (eqn_add2l a) => /eqP. move:(stern_fusc)=> [Ha Hb Hc Hd]. move:(leqnn m); elim: m n {-2} m. by move => n m; rewrite leqn0 => /eqP ->; rewrite leqn0 => /eqP ->. move => N Hrec n m; rewrite leq_eqVlt; case /orP; last first. by rewrite ltnS; apply: Hrec. move/eqP => -> nN. set u := n./2; set v := N.+1./2. case: (odd_dichot n); case: (odd_dichot N.+1) => ea eb; rewrite ea eb -/u -/v -? doubleS ?Hc ? Hd => sa sb. + move/eqP: sa; rewrite sb eqn_add2r => /eqP sa. have l1: u <= v by rewrite - leq_double -ltnS - eb - ea. have l2: v <= N by rewrite /v - leq_double - ltnS - ea double_le2. by rewrite (Hrec u v l2 l1 sa sb). + move: (esym sb); rewrite - sa => /aux /andP [_]. by rewrite eqn0Ngt stern_gt0. + move: sb; rewrite sa => /aux /andP [_]. by rewrite eqn0Ngt stern_gt0. + move/eqP: sb; rewrite sa eqn_add2l => /eqP sb. have l1: u <= v by rewrite - leq_double - eb - ea. have l2: v <= N. rewrite /v - leq_double - ea; move:(f_equal odd ea); clear; case N=>//. move => n _ ; apply: double_le3. by rewrite (Hrec u v l2 l1 sa sb). 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)