proposition: Lemma contraction_rec_succ' a n: natp n -> Vf (contraction_rec a) (csucc n) = Vf (contraction_rec (the_contraction a)) n.
proof: Proof. move => nN; move: n nN a; apply: Nat_induction. by move => a; rewrite (contraction_rec_succ _ NS0) ! contraction_rec0. move => n nN Hrec a. by rewrite (contraction_rec_succ _ (NS_succ nN)) Hrec contraction_rec_succ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)