proposition: Lemma nth_shape ss i : nth 0 (shape ss) i = size (nth [::] ss i).
proof: Proof. rewrite /shape; case: (ltnP i (size ss)) => Hi; first exact: nth_map. by rewrite !nth_default // size_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)