proposition: Lemma seq_subE s (s_gt0 : size s > 0) : s = map val (map (insubd (seq_sub_default s_gt0)) s : seq (seq_sub s)).
proof: Proof. by rewrite -map_comp map_id_in// => x x_in_s /=; rewrite insubdK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)