proposition: Lemma nth_belast (z : V) p i : nth z (belast z p) i = if i < size p then nth z (z :: p) i else z.
proof: Proof. rewrite lastI nth_rcons size_belast; have [i_lt|i_ge] //= := ltnP. by rewrite nth_default // size_belast. Qed.
imports: mathcomp(all_ssreflect) bigmin extra