proposition: Lemma contraction_rec_non_zero a n: natp n -> natp a -> a <> \0c -> (Vf (contraction_rec a) n) <> \0c.
proof: Proof. move => nN; move: n nN a; apply:Nat_induction. by move => a _ anz; rewrite contraction_rec0. move => n nN Hrec a aN anz; rewrite (contraction_rec_succ _ nN). apply:(the_contraction_non_zero (NS_contraction_rec aN nN) (Hrec _ aN anz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)