proposition: Lemma nat_to_B_injective: injective nat_to_B.
proof: Proof. elim. elim => // n h /= es; move: (@succ_nz (nat_to_B n)); rewrite -es //. move => n h; elim => [/= es | m h1 /= aux]. by move: (@succ_nz (nat_to_B n)); rewrite es. have cn := (CS_nat (nat_to_B_Nat n)). have cm:= (CS_nat (nat_to_B_Nat m)). congr (_ .+1); apply: h;exact: (csucc_inj cn cm aux). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)