proposition: Lemma fusc_bezout (a := fun n =>fusc (2^log2 n - n)) (c := fun n => if (n== 2^(log2 n).-1) then 0 else a n): (forall n, (c n.+1) * (fusc n) + 1 = (a n) *(fusc n.+1)).
proof: Proof. have Ha0: a 0 = 1 by []. have Hb0: c 1 = 0 by []. have Hae: (forall n, a (n.*2) = a n). by case => // n;rewrite /a log2_double expn2S - doubleB fusc_even. have Hbe: (forall n, c (n.*2) = c n). case => // n. by rewrite /c log2_double Hae succnK {1} log2S_k expn2S eqn_double. have Hao: (forall n, a (n.*2.+1) = a n + c n.+1). have exps k: (2^k).-1.+1 = 2^k by apply:prednK; rewrite expn_gt0. move => n; rewrite /c;move:(log2_bnd n) =>/andP[];rewrite leq_eqVlt eq_sym. case: eqP => eqa /= ha hb. have aux k: a ((2^k ).-1) = 1. by rewrite /a log2_pred_pow - {1} exps subSn // subnn. set k := (log2 n.+1).-1. have eqb: n = (2^k ).-1 by rewrite /k - eqa succnK. by rewrite eqb aux - (succnK (_.+1)) - doubleS exps - expn2S aux. rewrite /a. set k :=(log2 n.+1).-1. have: log2 n = k.+1 by apply:log2_pr;rewrite -ltnS ha /k -log2S_k (ltnW hb). move => ea; move: hb; rewrite log2_Sdouble ea log2S_k -/k => /ltnW hb. move:(subnK hb) (subnK (ltnW hb)); rewrite subnS; set x := _ - _ => sa sb. rewrite expn2S -addnn -addnn -addnS subnDA - (addnBA _ (ltnW hb)) addnC. rewrite - addnBA // subnS -/x; case x => //m. by rewrite succnK addSn addnn fusc_odd addnC. have Hbo: (forall n, c (n.*2.+3) = a n.+1 + c n.+2). move =>n; rewrite -(Hao n.+1) /c doubleS;case: eqP => //. case:((log2 n.*2.+3).-1) => //n1 h; move: (f_equal odd h). by rewrite expn2S /= !odd_double. elim /fusc_ind. + by rewrite muln0 Ha0. + move: (Hao 0)(Hbe 1); rewrite Ha0 Hb0 => -> -> //. + move => n Hr; rewrite fusc_even fusc_odd Hae mulnDr -Hr addnA - mulnDl. by case n; [rewrite !muln0 | move => k; rewrite doubleS Hbo]. + move => n Hr _. by rewrite Hao -doubleS Hbe fusc_even fusc_odd mulnDl mulnDr - Hr addnAC. 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)