proposition: Lemma minSS (p q : nat) : minn p.+1 q.+1 = (minn p q).+1.
proof: Proof. by rewrite /minn ltnS; case:ifP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly matrix mxpoly) CoqEAL(hrel param refinements trivial_seq)