proposition: Lemma fusc_palindrome i a b (p := 2 ^ i): p <= a <= p.*2 -> a + b = 3 * p -> fusc a = fusc b.
proof: Proof. rewrite /p => {p} sa sc. have sb: 2 ^ i <= b <= (2 ^ i).*2. rewrite - (leq_add2l a) - (leq_add2l a b) sc mulSn mul2n leq_add2r addnC. by rewrite leq_add2l andbC. move: sc => /eqP; elim: i a b sa sb. have H: forall c, 0 < c <=2 -> fusc c = 1 by case => //[][] // []. by rewrite expn0 => a b sa sb _; rewrite H // H. move => n Hrec a b; rewrite expn2S - doubleMr. rewrite -(odd_double_half a) -(odd_double_half b). case: (odd a); case: (odd b). + rewrite fusc_odd fusc_odd ! leq_Sdouble !ltn_double addSn addnS - doubleD. rewrite - doubleS eqn_double => /andP [sa sb] /andP [sc sd] se. rewrite addnC (Hrec a./2 b./2.+1) ?sa ? (leqW sc) ?sd ? (ltnW sb) ? addnS //. by rewrite (Hrec a./2.+1 b./2) ?sc ?(leqW sa) ?sb ? (ltnW sd) ? addSn. + move => _ _. by rewrite addSn - doubleD => /eqP /(f_equal odd); rewrite /= !odd_double. + move => _ _. by rewrite addnS - doubleD => /eqP /(f_equal odd); rewrite /= !odd_double. + rewrite fusc_even fusc_even !leq_double - doubleD eqn_double; apply: Hrec. 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)