proposition: Lemma N2N_part1: cardinal (Nat) <=c cardinal (coarse Nat).
proof: Proof. have: sub ((singleton \0c) \times Nat) (coarse Nat). by apply:setX_Sl => bt /set1_P ->; apply:NS0. by move/sub_smaller; rewrite (cardinal_indexedr Nat \0c). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)