proposition: Lemma the_contraction_non_zero a: natp a -> a <> \0c -> the_contraction a <> \0c.
proof: Proof. move => aN ap; rewrite /the_contraction. move: (the_expansion_pr aN). set f := (the_expansion a);move => [[pc pd] pe]. case: pe. move => /card_nonempty cdf; move: ap ; rewrite - pd. by rewrite /expansion_value/csumb csum_trivial //; aw. move: (pc) => [pg ph pi [pk1 pk2 pk3]] [pl pm] sz. move: (cpred_pr ph pl); set k1:= cpred _; move => [pn po]. have kh1:inc k1 (domain f). by rewrite pk2; apply/(NltP ph); rewrite po; apply:cltS. have ckf: cardinalp (Vg f k1) by move/pk3: kh1 => [[]]. by move: (csum_increasing6 ckf kh1); rewrite sz => /cle0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)