proposition: Lemma nat_to_B_quorem a b : nat_to_B(a %/ b) = (nat_to_B a) %/c (nat_to_B b) /\ nat_to_B(a %% b) = (nat_to_B a) %%c (nat_to_B b).
proof: Proof. case: (posnP b) => bp. by rewrite bp divn0 modn0 /= (crem_zero (nat_to_B_Nat a)) cquo_zero. move: (f_equal nat_to_B (divn_eq a b)). rewrite mulnC nat_to_B_sum nat_to_B_prod => h. apply: cquorem_pr;try apply:nat_to_B_Nat. by split => //; apply/nat_to_B_lt; apply:ltn_pmod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)