proposition: Lemma fusc_unique f g: fusc_prop f -> fusc_prop g -> {inc Nat, f =1 g}.
proof: Proof. move=> [Hf1 Hf2 Hf3 Hf4][Hg1 Hg2 Hg3 Hg4]. apply: fusc_induction. + by rewrite Hf1 Hg1. + by rewrite Hf2 Hg2. + by move => k kN eq; rewrite (Hf3 _ kN) (Hg3 _ kN) eq. + by move => k kN eq1 eq2; rewrite (Hf4 _ kN) (Hg4 _ kN) eq1 eq2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)