proposition: Lemma nat_to_B_surjective x: natp x -> exists n, x = nat_to_B n.
proof: Proof. move: x; apply: Nat_induction. by exists 0. by move=> n nN [m mv]; exists m.+1 ; rewrite mv //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)