proposition: Lemma sternD_coprime_succ_add i n (S := stern11 n) (a := nth 0 S i.-1)(b := nth 0 S i)(c := nth 0 S i.+1): 0 < i < 2 ^n -> b = a + c -> coprime a c.
proof: Proof. move => /andP[ha hb]. move:(sternD_consecutive_coprime1 hb) => sa sb. by move: sa; rewrite /coprime -/stern11 -/b sb gcdnC gcdnDr gcdnC. 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)