proposition: Lemma get_map_tab (t : seq (seq T1)) rc : in_shape (shape t) rc -> get_tab [seq [seq F i | i <- r0] | r0 <- t] rc = F (get_tab t rc).
proof: Proof. move=> Hin; have:= in_shape_size Hin; rewrite size_map => Hr. move: Hin; rewrite /in_shape (nth_map [::]) // /get_tab => Hc. by rewrite (nth_map [::] _ _ Hr) (nth_map inh). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted