proposition: Lemma sternD_nth_compare_rec u v n i: 0 < u -> 0 < v -> i.*2 < 2^n -> n < nth 0 (sternD u v n) i.*2.+1.
proof: Proof. move => sa sb;elim: n i. move => k; rewrite ltnS (leq_double k 0) leqn0 => /eqP -> //. move => n Hrec k; rewrite expn2S ltn_double => ha. move: (sternD_nth_compare_strict sa sb ha). rewrite - doubleS !sternD_nth_even gtn_max; move/andP => [hc hd]. case: (odd_dichot k) => k1; rewrite k1 in ha. by apply: leq_trans hc; rewrite ltnS k1; apply: Hrec; apply: ltnW. by apply: leq_trans hd; rewrite ltnS k1; apply: Hrec. 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)