proposition: Lemma even_double n: natp n -> evenp (cdouble n).
proof: Proof. move => h; split; first by apply: NS_double. exact: (proj33 (cdivides_pr1 h NS2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)