proposition: Lemma the_contraction_zero: the_contraction \0c = \0c.
proof: Proof. by rewrite /the_contraction the_expansion_zero csum_trivial // domain_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)