proposition: Lemma fusc_compare1 i j k: i < j -> i + j = 2 ^ k -> fusc i < fusc j.
proof: Proof. elim : k i j. rewrite expn0; case; first by move => j _; rewrite add0n => ->. move => i j lij /eqP; rewrite addSn eqSS addn_eq0 => /andP[ha hb]. move: lij; rewrite (eqP ha) (eqP hb) //. move => n H i j lij sij. have oij: (odd (i + j)) == false by rewrite sij expn2S odd_double. case: (odd_dichot i) => iv; case:(odd_dichot j) => jv. + move /eqP: sij. rewrite iv jv addnS addSn -doubleD -doubleS expn2S eqn_double -addnS => /eqP. move => ha; move:(ha); rewrite -addSnnS => hb. have hc: i./2 < j./2.+1 by rewrite ltnS -leq_double -ltnS -iv -jv; apply:ltnW. case xx: (i./2.+1 == j./2). by rewrite !fusc_odd (eqP xx) addnC ltn_add2l H. have hd: i./2.+1 < j./2 by rewrite ltn_neqAle xx -ltn_double -ltnS -iv -jv. by rewrite !fusc_odd addnC -addnS leq_add // ?(ltnW (H _ _ hd hb)) // H. + by move: oij; rewrite iv jv oddD /= !odd_double. + by move: oij; rewrite iv jv oddD /= !odd_double. + rewrite iv jv !fusc_even; apply:H; first by rewrite - ltn_double - iv -jv. by apply/eqP; rewrite - eqn_double doubleD - iv - jv sij expn2S. 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)