proposition: Lemma contraction_rep_dig a : natp a -> contraction_rep a <c b.
proof: Proof. move:a. suff: forall a, natp a -> forall c, c <=c a -> contraction_rep c <c b. move => H a aN; exact: (H a aN a (cleR (CS_nat aN))). apply: Nat_induction. move => c /cle0 ->; rewrite /contraction_rep contraction_rec0. exact:(clt_ltT (clt_01) bp). have H: forall n, natp n -> forall a, a <c b -> Vf (contraction_rec a) n = a. apply: Nat_induction; first by move => a _; rewrite contraction_rec0. move => n nN Hrec a ab; rewrite (contraction_rec_succ' _ nN). rewrite (the_contraction_digit ab); exact: Hrec. move => n nN Hrec c csn; case: (equal_or_not c (csucc n)); last first. move => h;move /(cltSleP nN): (conj csn h); exact: Hrec. have snN:=(NS_succ nN). move => ->; case: (NleT_el bN snN) => cnb; last first. by rewrite/contraction_rep (H _ snN _ cnb). move:(the_contraction_non_digit cnb snN) => /(cltSleP nN). rewrite /contraction_rep (contraction_rec_succ' _ nN). set x := the_contraction (csucc n) => xn. move: (NS_le_nat xn nN) (NS_diff x nN) (Hrec _ xn) => ha hb hc. rewrite -(cdiff_pr xn) (contraction_rec_succ'' _ ha hb). by rewrite -/(contraction_rep _) (H _ hb _ hc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)