proposition: Lemma sternD_1n_kl_sym n q i j (k := stern j) (l := stern i): i + j = 2^q -> nth 0 (sternD 1 n q) i = k + n * l /\ coprime k l.
proof: Proof. rewrite /k/l => sb. have sc: i <= 2 ^q by rewrite -sb leq_addr. by rewrite sternD_1n_kl// -sb addKn !sternD_fusc coprime_sym (fusc_fusc3 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)