proposition: Lemma the_contraction_non_digit a: b <=c a -> natp a -> the_contraction a <c a.
proof: Proof. move => pa pb; rewrite /the_contraction. move: (the_expansion_pr pb). set f := (the_expansion a);move => [[pc pd] pe]. case: pe. move => /card_nonempty cdf; rewrite csum_trivial //. exact: (clt_leT (clt_ltT clt_01 bp) pa). move: (pc) => [pg ph pi [pk1 pk2 pk3]] [pl pm]. move: (cpred_pr ph pl); set k1:= cpred _; move => [pn po]. move:pm; rewrite po; rewrite (cpred_pr2 pn) => pm. set g := (Lg (domain f) (fun i => Vg f i *c b ^c i)). have fsdf: finite_set (domain f) by rewrite /finite_set po; fprops. have dfdg: domain f = domain g by rewrite /g; aw. have qa:finite_int_fam f. split => //; move => i /pk3 h; apply:(NS_lt_nat h pg). have qb:finite_int_fam g. rewrite /g; saw; hnf; aw => i idf. rewrite LgV //; move: (proj1 qa _ idf) => sa; apply/NS_prod => //. apply /NS_pow => //. by move: idf; rewrite pk2 po; move/(NleP pn) => le; move:(NS_le_nat le pn). rewrite - pd /expansion_value /csumb. have bsp:= (clt_ltT (clt_01) pi). apply: (finite_sum_lt qa qb); aw; trivial. rewrite /g; move => i idf;rewrite LgV //; apply: cprod_M1le. exact: (CS_nat (proj1 qa _ idf)). by apply: cpow_nz => bz; case: (proj2 bsp). have kh1:inc k1 (domain f). by rewrite pk2; apply/(NltP ph); rewrite po; apply:cltS. have nk1: natp (Vg f k1) by apply(proj1 qa _ kh1). have nk3: natp (b ^c k1) by fprops. case: (equal_or_not k1 \0c) => k1z. have ddf: domain f = singleton \0c. by rewrite pk2 po k1z succ_zero. have zdf: inc \0c (domain f) by rewrite ddf; fprops. have aux:= (CS_nat (proj1 qa _ zdf)). have rs: Vg f \0c *c b ^c \0c = Vg f \0c. by rewrite cpowx0 (cprod1r aux). case:(cleNgt pa);move: pd (pk3 _ zdf). by rewrite /expansion_value ddf (csum_trivial3) rs (card_card aux) => ->. have pp:= (clt_leT pi (cpow_Mle1 (CS_nat pg) k1z)). exists k1 => //; rewrite /g; rewrite LgV //; apply:cprod_M1lt => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)