proposition: Lemma contraction_rec_succ a n: natp n -> Vf (contraction_rec a) (csucc n) = the_contraction (Vf (contraction_rec a) n).
proof: Proof. exact: (proj44 (induction_defined_pr (the_contraction) a) n). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)