proposition: Lemma DUR_exclusion1 i: v i + v i.+2 != v i.+1.
proof: Proof. case eqP => // eq1. set l := iota 0 i. set l1 := rev(rcons (rcons l i) i.+2). set l2 := rev (rcons l i.+1). have ea:Zval_v l1 = Zval_v l2. by rewrite /Zval_v /l1 /l2 !sum_rev !sum_rcons addnA (addnC _ (v i)) eq1. 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 (iota 0 i.+2)). congr rev; rewrite /l iota_Sr iota_Sr ! add0n; rewrite rem_rcons1 //. by rewrite rem_rcons2 // mem_iota ltnn andbF. have sa: spec_sorted l1 by rewrite eb; apply: iota_rem_spec_sorted. have sb: spec_sorted l2 by rewrite ec; apply: iota_rem_spec_sorted. move:(v_unique sa sb ea); rewrite eb ec => /rev_inj => ed. move: (f_equal size ed); rewrite !size_rem ?size_iota ? mem_iota ?ltnS //=. by move/esym /n_Sn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)