proposition: Lemma sternD_1n_coprime n q i: i < 2^q -> exists K L, coprime K L /\ nth 0 (sternD 1 n q) i = K + n*L.
proof: Proof. move => h; move: (sternD_1n_bezout n h) => [-> _]. rewrite mulnC => /coprime_if_bezout. by exists (stern (2 ^ q - i)), (stern i). 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)