proposition: Lemma nat_to_B_diff x y: nat_to_B (x - y) = nat_to_B x -c nat_to_B y.
proof: Proof. case: (ltnP x y) => p1. move: (ltnW p1) => p2. have -> /= : x -y = 0 by apply /eqP. rewrite /cdiff. by move / nat_to_B_le : p2 => [_ _ /setC_T ->]; rewrite cardinal_set0. rewrite - {2}(subnK p1) nat_to_B_sum cdiff_pr1 //; apply:nat_to_B_Nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)