proposition: Lemma fusc_bound i n: i <= 2 ^n -> fusc i <= fusc (2 ^ n + i) ?= iff (i == 2 ^ n).
proof: Proof. move => h; rewrite -(fusc_symmetry1 h). apply/leqifP; case hb: (i == 2 ^ n);first by rewrite (eqP hb) subnn add0n eqxx. by apply/ltn_paddl; rewrite lt0n fusc_eq0 - lt0n subn_gt0 ltn_neqAle h hb. 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)