proposition: Lemma NS_esize c: echelon c -> natp (esize c).
proof: Proof. move => h. have sN:=(proj2 (proj1 (proj1 h))). case (equal_or_not (domain c) \0c) => sz. rewrite (esize_empty h sz); apply: NS0. by case:(esize_prop1 h (card_ne0_pos (CS_nat sN) sz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)