proposition: Lemma sternD_1n_bezout n q i (S := sternD 1 n q) (k:= stern (2 ^ q - i)) (l:= stern i) (k':= stern (2 ^ q - i.+1)) (l':= stern i.+1): i < 2^q -> [/\ nth 0 S i = k + n * l, nth 0 S i.+1 = k' + n * l' & k * l' = k' * l + 1 ].
proof: Proof. rewrite (mulnC k) (mulnC k') /S/k/k'/l/l'; clear. case:q. have s0: stern 0 = 0 by []. have s1: stern 1 = 1 by []. by rewrite ltnS leqn0 => /eqP -> //=; rewrite s0 s1 muln0 muln1. have HA: forall i q, i < 2^q -> stern i.+1 * stern (2 ^ q.+1 - i) = stern i * stern (2 ^ q.+1 - i.+1) + 1. move => j q liq; move: (ltnW liq) => liq'. move:(proj1 (fusc_bezout_minimal liq)). rewrite -!sternD_fusc - !nth_stern11 // !nth_stern11_sym //. move => q liq. rewrite (sternD_1n_kl _ (ltnW liq)) (sternD_1n_kl _ liq); split => //. case (ltnP i (2^q)) => ha; first by apply: HA. set j := 2^ q.+1 - i.+1. have hc: (2 ^ q.+1 - j) = i.+1 by rewrite- (subnK liq) -/j addKn. have hd: (2 ^ q.+1 - j.+1) = i by rewrite subnS hc. have j': (2 ^ q.+1 - i) = j.+1 by rewrite -(subnK liq) -/j -addSnnS addnK. have ljq: j < 2^q. by rewrite -(leq_add2r i) /j addSnnS subnK // expn2S -addnn leq_add2l. rewrite j' (mulnC _ (stern j.+1)) (mulnC _ (stern j)). by move: (HA j q ljq); rewrite hc hd. 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)