proposition: Lemma the_contraction_digit a: a <c b -> the_contraction a = a.
proof: Proof. move => lab. case: (equal_or_not a \0c) => anz. by rewrite anz; exact:the_contraction_zero. rewrite /the_contraction - {2} (card_card (proj31_1 lab)) /the_contraction. move: (simple_fct2 \0c a) => [_ _ _ _ re]. by rewrite (the_expansion_digit anz lab) re -/(csumb _ _ ) csum_trivial3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)