proposition: Lemma Fib_fusc_rec1: Fib_fusc_rec (csucc \0c) = (J \1c \0c).
proof: Proof. rewrite (Fib_fusc_recS NS0) Fib_fusc_rec0 pr2_pair cdouble0 succ_zero. by rewrite pr1_pair (csum0r CS0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)