proposition: Lemma double_succ a: natp a -> cdouble (csucc a) = csucc (csucc (cdouble a)).
proof: Proof. move => aN; move:(NS_double aN) => dN. rewrite (Nsucc_rw aN) - double_sum {2} /cdouble (cprod1r CS2) - csum_11. by rewrite csumA -(Nsucc_rw dN) - (Nsucc_rw (NS_succ dN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)