proposition: Lemma DUR_injv: injective v.
proof: Proof. move => i j sv. set l:= iota 0 (i+j).+1. have Ha: forall k, k\in l -> Zval_v l = Zval_v (k :: rem k l). by move => k H; apply: perm_big; apply:perm_to_rem. have il: i \in l by rewrite mem_iota /= ltnS leq_addr. have : Zval_v (i :: rem i l) = Zval_v (j :: rem j l). by rewrite - Ha // - Ha // mem_iota /= ltnS leq_addl. move/eqP; rewrite /Zval_v !big_cons sv eqn_add2l - sum_rev. rewrite - [ X in _ == X] sum_rev => /eqP eq1. have Hb:= (iota_rem_spec_sorted (i+j).+1). move: (v_unique (Hb i) (Hb j) eq1) => /rev_inj eq2. case ok:(i== j); first by rewrite (eqP ok). have ul: uniq l by apply: iota_uniq. have: i \in rem j l by rewrite mem_rem_uniq // inE ok. by rewrite - eq2 mem_rem_uniq // inE // eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)