proposition: Lemma incr_nthC v i j : incr_nth (incr_nth v i) j = incr_nth (incr_nth v j) i.
proof: Proof. apply: (@eq_from_nth _ 0) => [|k _]; last by rewrite !nth_incr_nth addnCA. by do !rewrite size_incr_nth leqNgt if_neg -/(maxn _ _); apply: maxnAC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)