proposition: Lemma sternD_bezout n i (f := fun n i => nth 0 (stern11 n) i): i < 2 ^n -> (f n i) * (f n.+1 i.+1) = 1 + (f n i.+1) * (f n.+1 i).
proof: Proof. move => h; move: (ltnW h) => h1. have h2: i < 2 ^ n.+1 by rewrite expn2S -addnn; apply:ltn_addr. move: (ltnW h2) => h3. rewrite /f !nth_stern11 // !sternD_fusc ! fusc_col_progression //. by rewrite ! mulnDr mulnC addnCA fusc_bezout2. 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)