proposition: Lemma incr_nth_inj v : injective (incr_nth v).
proof: Proof. move=> i j /(congr1 (nth 0 ^~ i)); apply: contra_eq => neq_ij. by rewrite !nth_incr_nth eqn_add2r eqxx /nat_of_bool ifN_eqC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)