proposition: Lemma contraction_rep_non_zero a: natp a -> a <> \0c -> (contraction_rep a) <> \0c.
proof: Proof. by move => pa pb; apply:(contraction_rec_non_zero pa pa pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)