proposition: Lemma fuscp_injective n m: fusc n = fusc m -> fusc n.+1 = fusc m.+1 -> n = m.
proof: Proof. wlog H: n m / n <= m. by move => H ? ?; case /orP:(leq_total n m) => sc; [ | symmetry]; apply: H. elim: m n H => [ [] | n H] // [_ |m]. by move => /eqP; rewrite fusc0 eq_sym fusc_eq0. rewrite ltnS => sa sb sc; congr succn; apply: H => //. by rewrite fusc_prevE (fusc_prevE n) sb sc. 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)