proposition: Lemma cpred_double n: natp n -> cpred (cpred (cdouble n)) = cdouble (cpred n).
proof: Proof. move => nN; case: (equal_or_not n \0c) => nz. by rewrite nz /cdouble cpred0 cprod0r !cpred0. move: (cpred_pr nN nz) => [sa {1} ->]; rewrite (double_succ sa). move: (NS_double sa) => sb; move:(NS_succ sb)=> sc. rewrite !cpred_pr2 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)