proposition: Lemma fusc_fusc3 n m p: n + m = 2^p -> coprime (fusc n) (fusc m).
proof: Proof. wlog: n m/ n <= m. move => H; move: (leq_total n m); case /orP; first by apply: H. move => ba; rewrite coprime_sym addnC => q; exact:(H _ _ ba q). case: p. move => _ /eqP;case: n; first by rewrite add0n;move/eqP => ->. by move => n; rewrite addSn eqSS addn_eq0 => /andP [/eqP -> /eqP ->]. move => p;case: m; first by rewrite addn0 => _ ->; rewrite fusc_pow2. move => m; case: (elogn2P m) => k q -> leq2 eq2. move:(leq_addl n (2 ^ k * q.*2.+1)); rewrite eq2 => l1. have pp:0 < 2^k by rewrite expn_gt0. have: 0 < q.*2.+1 by rewrite ltnS. rewrite -(leq_pmul2l pp) muln1 => eq3. move: (leq_trans eq3 l1); rewrite leq_exp2l // => lekp. move: eq2; rewrite -{1}(subnK lekp) (addnC _ k) expnD => eq2. move:(addnK (2 ^ k * q.*2.+1) n); rewrite eq2 - mulnBr => eq4. rewrite - eq4 ! fusc_kpow2n;set w := (2 ^ (p.+1 - k) - q.*2.+1). have: w <= q.*2.+1 by rewrite -(leq_pmul2l pp) eq4. move/eqP: eq2; rewrite -eq4 -mulnDr eqn_mul2l expn_eq0 -/w /=;case: (p.+1 - k). rewrite addnS eqSS addn_eq0 => /andP [/eqP -> /eqP -> //]. move:(w);clear; move => w p eq1. rewrite leq_eqVlt; case/orP => le1. move: eq1;rewrite (eqP le1) addnn expn2S eqn_double => /eqP ->. by rewrite fusc_pow2. have ok: odd (q.*2.+1) by rewrite /= odd_double. have /andP[ le3 le4]: w <2^p <= q.*2.+1. rewrite -(leq_add2l w (2^p) q.*2.+1); move: (ltn_add2l w w q.*2.+1). rewrite (eqP eq1) le1 expn2S addnn ltn_double - addnn leq_add2r=> h. by rewrite h /= (ltnW h). have ln: log2 (q.*2.+1) = p.+1. apply: log2_pr;rewrite le4 /=; case:(posnP w) => wp. by move: ok;rewrite - (add0n q.*2.+1) - wp (eqP eq1) expn2S odd_double. by rewrite -(eqP eq1) - (prednK wp) addSn ltnS leq_addl. have oiq:= (bin_invert_odd ok). set n := base2rev(bin_invert (q.*2.+1)). have eq3: bin_invert (base2rev n) = q.*2.+1. by rewrite /n (base2rev_oddI oiq) bin_invertI. case: (posnP (bin_invert q.*2.+1)) => sa; first by move: oiq; rewrite sa /=. case: (posnP n) => nz; first by move:eq3; rewrite nz //. have on : odd n by rewrite /n - (prednK sa); apply: odd_base2rev. rewrite - eq3 fusc_bin_invert fusc_reverse. case en1:(n==1); first by rewrite (eqP en1) /coprime fusc1 /= gcdn1. move: (log_base2r oiq) eq1; rewrite log2_bin_invert -/n ln => <-. rewrite - eq3 - (base2_rev_invert on (negbT en1)) eqn_add2r => /eqP ->. rewrite fusc_reverse -{2}(prednK nz);apply:fusc_coprime. 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)