proposition: Lemma fusc_bezout2 i n: i < 2^n -> fusc (2 ^ n + i) * fusc i.+1 = 1 + fusc (2 ^ n + i.+1) * fusc i.
proof: Proof. elim /fusc_ind: i n. + by move => n; rewrite fusc0 fusc1 addn0 addn1 fusc_pow2 fusc_succ_pow2 muln0. + move => n;rewrite fusc1 fusc2 ! muln1 addn1 fusc_succ_pow2; case: n => //. by move => n _; rewrite expn2S addn2 -doubleS fusc_even fusc_succ_pow2 add1n. + move => i H; case. rewrite expn0 ltnS (leq_double i 0) leqn0 => /eqP -> //. move =>n; rewrite expn2S ltn_double addnS -doubleD !fusc_even !fusc_odd => ha. by rewrite mulnDr mulnDl H // addnCA addnS. + move => i Ha Hb; case; first by rewrite ltnS ltn0. move => n. rewrite expn2S ltn_Sdouble !addnS - doubleD -!doubleS => ha. by rewrite !fusc_even !fusc_odd mulnDr mulnDl Ha // addnS addnA. 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)