proposition: Lemma fusc_unique f g: fusc_prop f -> fusc_prop g -> f =1 g.
proof: Proof. move => [pa pb pc pd] [qa qb qc qd] n. elim /fusc_ind: n => //. + by rewrite pa qa. + by rewrite pb qb. + by move => n h; rewrite pc qc. + by move => n h1 h2; rewrite pd qd h1 h2. 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)