proposition: Lemma double_inj a b: natp a -> natp b -> cdouble a = cdouble b -> a = b.
proof: Proof. by move => aN bN; move/(cprod_eq2l NS2 aN bN card2_nz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)