proposition: Lemma fusc2_injective n m: fusc n = fusc m -> fusc n.+1 = fusc m.+1 -> n = m.
proof: Proof. wlog H: n m / n <= m. move => Hrec sa sb; case /orP:(leq_total n m) => sc; first by apply: Hrec. symmetry; apply: Hrec => //. have aux a b c: b +a + c = a -> (b==0) && (c == 0). by rewrite (addnC b) -addnA -{2} (addn0 a) - addn_eq0 - (eqn_add2l a) => /eqP. elim /fusc_ind: m n H => [n | n | n Hrec m | n Hrec _ m]. + by rewrite leqn0 => /eqP. + rewrite leq_eqVlt; case/orP; first by move/eqP => ->. by rewrite /fusc ltnS leqn0 => /eqP -> /=. + rewrite - (odd_double_half m); case: (odd m); rewrite - ?doubleS !fusc_even !fusc_odd. by move => _ <- /esym /aux; rewrite !fusc_eq0 andbF. rewrite leq_double => /Hrec h1 h2 /eqP;rewrite h2 eqn_add2l => /eqP h3. by rewrite h1. + rewrite - (odd_double_half m); case: (odd m); rewrite - !doubleS !fusc_even !fusc_odd. rewrite ltnS leq_double => /Hrec h1 /eqP h2 h3. by move: h2; rewrite h3 eqn_add2r => /eqP h2; rewrite h1. by move => _ -> /aux;rewrite !fusc_eq0 andbF. 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)