proposition: Lemma NS_contraction_rec a n: natp a -> natp n -> natp (Vf (contraction_rec a) n).
proof: Proof. move => aN nN; move: n nN a aN; apply: Nat_induction. by move => a aN; rewrite contraction_rec0. move => n nN Hrec a /Hrec aN; rewrite (contraction_rec_succ _ nN). case: (NleT_el bN aN) => cnb. by move:(the_contraction_non_digit cnb aN) => /(NS_lt_nat); apply. by rewrite (the_contraction_digit cnb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)