proposition: Lemma DUR_exclusion2 i: v i + v i.+2 != v i.+1 + v i.+3.
proof: Proof. case eqP => // eq1. set l := iota 0 i. set l1 := rev(rcons (rcons l i) i.+2). set l2 := rev (rcons (rcons l i.+1) i.+3). have ea:Zval_v l1 = Zval_v l2. rewrite /Zval_v /l1 /l2 !sum_rev !sum_rcons !addnA (addnC _ (v i)) eq1. by rewrite (addnC _ (v i.+1)). have eb: l1 = rev (rem i.+1 (iota 0 i.+3)). congr rev; rewrite iota_Sr iota_Sr add0n rem_rcons1 //. by rewrite - iota_Sr rem_rcons2 // mem_iota ltnn andbF. have ec: l2 = rev (rem i.+2 (rem i (iota 0 i.+4))). have ha: i < i.+3 by rewrite !ltnS; apply: (@leq_trans i.+1). have hb: i \notin iota 0 i by rewrite mem_iota ltnn andbF. congr rev; rewrite ! iota_Sr !add0n rem_rcons1 // rem_rcons1 //. rewrite rem_rcons1 // rem_rcons2 // rem_rcons1 // rem_rcons2 //. by rewrite mem_rcons inE mem_iota /= negb_or gtn_eqF //= - leqNgt. have sa: spec_sorted l1 by rewrite eb; apply: iota_rem_spec_sorted. have sb: spec_sorted l2 by rewrite ec; apply: iota_rem2_spec_sorted. move:(v_unique sa sb ea); rewrite eb ec => /rev_inj => ed. have: i.+2 \in rem i.+1 (iota 0 i.+3). rewrite 2!iota_Sr !add0n rem_rcons1 // rem_rcons2 // ?mem_iota ?ltnn //. by rewrite mem_rcons inE eqxx. rewrite ed mem_rem_uniq ?inE ?eqxx //; apply/ rem_uniq/iota_uniq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)