proposition: Lemma fusc_coprime1 n: fusc n + fusc n.+2 = fusc (n.+1) -> coprime (fusc n) (fusc n.+2).
proof: Proof. case: (elogn2P n) => k q ea. move:(fusc_middle_div k q) => /=; rewrite -ea succnK => -> /eqP. rewrite mulnC mulnSr - {3} (add0n (fusc n.+1)) eqn_add2r muln_eq0 fusc_eq0 //=. rewrite - mul2n muln_eq0/= => /eqP kz; move:ea; rewrite kz mul1n => /eq_add_S. move =>->; rewrite - doubleS !fusc_even; 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)