proposition: Lemma fusc_fusc2 a b: coprime a b -> exists n m p, [/\ n + m = 2^p, a = fusc n & b = fusc m].
proof: Proof. wlog: a b/ a <= b. move => H; move: (leq_total a b); case /orP; first by apply: H. move => ba; rewrite coprime_sym => q; move:(H _ _ ba q). by move => [n [m [p [ea -> ->]]]]; exists m, n, p; rewrite addnC. case: a; first by rewrite /coprime gcd0n => _ /eqP -> ;exists 0,1,0. move => a; case: b; first by rewrite /coprime gcdn0 => _ /eqP ->;exists 1,0,0. move => b h cp; move: h ;move:(fusc_pair_surj cp) => [k [ -> ->]]. case ok: (odd k). by rewrite leqNgt; case: (fusc_monotone ok) => -> //; exists 1,1,1. case kz: (k ==0); first by rewrite (eqP kz); exists 0,1,0. exists (base2rev k.+1.-1), (bin_invert (base2rev k.+1)),(log2 k.+1); split. + by apply:base2_rev_invert => /=; rewrite ?ok //eqSS kz. + by rewrite succnK fusc_reverse. + by rewrite fusc_bin_invert fusc_reverse. 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)