proposition: Lemma sternD_gcd_succ u v i n (S := sternD u v n): 0 < i < 2^n -> gcdn (nth 0 S i.-1) (nth 0 S i) = gcdn (nth 0 S i)(nth 0 S i.+1).
proof: Proof. move => h. move: (sternD_middle_div u v h). set b := nth _ _ _; set a := nth _ _ _; set c := nth _ _ _ => /dvdnP [k ks]. have ea: c = k* b - a by rewrite - ks addKn. have lab: a <= k * b by rewrite -ks leq_addr. have eb: a = k* b - c by rewrite - ks addnK. have lac: c <= k * b by rewrite -ks leq_addl. move: (dvdn_gcdr a b) (dvdn_gcdl a b) => da db. move: (dvdn_gcdr b c) (dvdn_gcdl b c) => dc dd. have ha: gcdn a b %| k * b by rewrite dvdn_mull. apply/eqP; rewrite eqn_dvd ! dvdn_gcd da dd {1} ea dvdn_subr // db. by rewrite eb dvdn_subr // ? dc // dvdn_mull. 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)