proposition: Lemma esize_empty c : echelon c -> slength c = \0c -> esize c = \0c.
proof: Proof. move => [[ec _] _] sz. rewrite /esize (slist_domain ec) sz Nint_co00 /Lg funI_set0 range_set0. by rewrite setU_0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)