proposition: Lemma fusc_coprime_palindrome i a b (p := 2 ^ i): p <= a <= p.*2 -> (a + b).+1 = 3 * p -> coprime (fusc a)(fusc b).
proof: Proof. rewrite -addnS => sa sb. by rewrite (fusc_palindrome sa sb) coprime_sym; 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)