proposition: Lemma set_last_default (T : eqType) y0 x0 (s : seq T) : size s > 0 -> last x0 s = last y0 s.
proof: Proof. by move=> s_gt0; rewrite -!nth_last; apply/set_nth_default; rewrite ?prednK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin