proposition: Lemma nth_vctmin v1 v2 i : nth 0 (vctmin v1 v2) i = minn (nth 0 v1 i) (nth 0 v2 i).
proof: Proof. rewrite /vctmin. case: (ltnP i (minn (size v1) (size v2))) => Hi. - rewrite (nth_map (0,0)) ?size_zip //=. by rewrite !nth_zip_cond ?size_zip Hi /=. - rewrite nth_default; last by rewrite size_map size_zip. move: Hi. by rewrite geq_min => /orP[] /(nth_default 0) ->; rewrite ?min0n ?minn0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype