proposition: Lemma DUR_01 : v 0 = 1 /\ v 1 = 2.
proof: Proof. have Ha a b l: spec_sorted [:: a, b & l] -> 2 < Zval_v (a::b::l). move => /spec_sorted_sorted nab; rewrite /Zval_v !big_cons addnA. apply:(@leq_trans ( v a + v b)); last by apply leq_addr. move:(DUR_positive a) (DUR_positive b) => ha hb. move: ha; rewrite leq_eqVlt => /orP; case => ha; last exact:(leq_add ha hb). move: hb;rewrite leq_eqVlt => /orP; case=> hb;last by rewrite -(eqP ha) ltnS. have eab: a = b by apply:DUR_injv; rewrite - (eqP ha) -(eqP hb). by move/andP: nab=> []; rewrite eab /gtn /= ltnn. move: (v_exists 2) => [[| b l]]; first by rewrite /Zval_v big_nil //. case:l; last by move => a l /Ha ha hb; move: ha; rewrite hb. rewrite spec_sorted_rec /Zval_v big_cons big_nil addn0/= => /andP [pa _] pb. move: (v_exists 1) => [[| a l]]; first by rewrite /Zval_v big_nil //. case:l; last by move => c l /Ha ha hb; move: ha; rewrite hb. rewrite spec_sorted_rec /Zval_v big_cons big_nil addn0/= => /andP [pc _] pd. move: pc; rewrite leqn1; case/orP => /eqP pc. rewrite - pb - {1} pd; move: pa; rewrite leqn1; case/orP => /eqP pa. have //: 1 = 2 by rewrite - pb - pd pa pc. by rewrite pa pc. move: pa; rewrite leqn1; case/orP => /eqP pa; last first. have //: 1 = 2 by rewrite - pb - pd pa pc. move: pb pd; rewrite pa pc => v0 v1; clear a b pa pc. have Hb: forall i, 2 <= i -> 3 <= v i. move => i i2;rewrite !ltn_neqAle; case: eqP. by rewrite - v0; move/DUR_injv => h; move: (ltnW i2); rewrite h ltnn. case: eqP; first by rewrite -v1;move/DUR_injv => h; move: i2; rewrite h ltnn. by rewrite eq_sym (lt0n_neq0 (DUR_positive i)). have Hc a b c l: spec_sorted [:: a, b,c & l] -> 6 <= Zval_v (a::b::c::l). move => /spec_sorted_sorted nab; rewrite /Zval_v !big_cons !addnA. apply:(@leq_trans (v a + v b + v c)); last by apply leq_addr. move: nab => /= /andP [lta /andP [ltb _]]. move: (leq_ltn_trans (leq0n c) ltb); rewrite - ltnS => ltc. move:(Hb _ (leq_trans ltc lta)) => ltd; case:(leqP b 1). rewrite leqn1; case/orP => /eqP bv; move:ltb; rewrite bv //. by rewrite ltnS leqn0 => /eqP ->; rewrite v0 v1 addn1 addn2 !ltnS. move/Hb => lte; move:(leq_add ltd lte) => ltf;apply(leq_trans ltf). by rewrite leq_addr. have Hd: Zval_v [::] = 0 by rewrite / Zval_v big_nil. have He a:spec_sorted [:: a] -> Zval_v [:: a] <= 2. rewrite spec_sorted_rec /= /Zval_v big_cons big_nil addn0. by rewrite leqn1; case/andP; case/orP => /eqP ->; rewrite ?v0 ?v1. move: (v_exists 4) => [l]. case:l; [by rewrite Hd | move => a4]; case; last move => b4. by move/He => h1 h2; move: h1; rewrite h2. case; last by move => c4 l /Hc => h1 h2; move: h1; rewrite h2. move: (v_exists 5) => [l]. case:l; [by rewrite Hd | move => a5]; case; last move => b5. by move/He => h1 h2; move: h1; rewrite h2. case; last by move => c4 l /Hc => h1 h2; move: h1; rewrite h2. rewrite !spec_sorted_rec /spec_sorted /= ! andbT. rewrite /Zval_v !big_cons !big_nil !addn0 => /andP [pa pb] pc /andP [pe pf] pg. move:pb; rewrite leqn1;case/orP => /eqP eq1; move: pc; rewrite eq1; last first. rewrite v1 addn1 => /eqP; rewrite eqSS => /eqP va5. move: pf; rewrite leqn1;case/orP => /eqP eq2; move: pg; rewrite eq2. rewrite v0; move => /eqP; rewrite addn2 eqSS eqSS - v0=> /eqP /DUR_injv. by move => ba; move: pe;rewrite eq2 ba //. rewrite v1 addn1 => /eqP; rewrite eqSS => /eqP va4; rewrite eq2 in pe. rewrite eq1 in pa; case/orP: pa => /eqP ea; case/orP: pe => /eqP eb. + by move: va5 va4; rewrite ea eb => ->. + by move:(DUR_exclusion1 1); rewrite v1 - eb va4 - {2} ea va5 //. + by move:(DUR_exclusion2 0); rewrite - {1} ea - {1} eb v0 v1 va4 va5. + by move: va5 va4; rewrite ea eb => ->. rewrite v0 addn2 => /eqP; rewrite !eqSS => /eqP va5. move: pa va5; rewrite eq1; case /orP => /eqP ->;first by rewrite v1 //. move => v2; clear a4 b4 a5 b5 pe pf pg eq1. have Hf: v 3 != 4. by apply/negP => /eqP v3; move:(DUR_exclusion2 0); rewrite v0 v1 v2 v3. have Hg i: 3 <= i -> 4 <= v i. move=> ha;rewrite !ltn_neqAle; case: eqP. by rewrite - v2; move/DUR_injv => h; move: ha; rewrite h ltnn. case: eqP; first by rewrite - v0; move/DUR_injv => h; move: ha; rewrite -h. case: eqP; first by rewrite -v1;move/DUR_injv => h; move: ha; rewrite -h. by rewrite eq_sym (lt0n_neq0 (DUR_positive i)). have Hi a b c d l: spec_sorted [:: a, b, c, d & l] -> 10 <= Zval_v [:: a, b, c, d & l]. move => H; move:(H). move => /spec_sorted_sorted /= /andP [lta /andP [ltb /andP [ltc _]]]. have w: 3 <= d.+3 by []. rewrite - 2!ltnS in ltc; rewrite - ltnS in ltb. move: (leq_trans w (leq_trans (leq_trans ltc ltb) lta)) => /Hg la. move: H; rewrite spec_sorted_rec => /= /andP [_ /Hc] lb. rewrite /Zval_v (big_cons); exact:(leq_add la lb). move:(v_exists 7) => [l]. case:l; [by rewrite Hd | move => a7]; case. by move/He => h1 h2; move: h1; rewrite h2. move => b7; case; last first. have Hj i: 3 < i -> v i + v 3 == 6 -> False. move => ha hb. by move: (leq_add (Hg _ (ltnW ha)) (Hg 3 (leqnn 3))); rewrite (eqP hb). move => c7; case; last by move => a l /Hi => h1 h2; move: h1; rewrite h2. rewrite !spec_sorted_rec /spec_sorted /= ! andbT. rewrite /Zval_v !big_cons big_nil addn0 leqn1. case/and3P; case/orP => /eqP ea; case/orP => /eqP eb; case/orP => /eqP ec; rewrite ea eb ec ?v0 ?v1 ?v2 => /eqP. + done. + by rewrite -[7]/(3 + (3 +1)) (eqn_add2r) -{2} v2 => /eqP/DUR_injv. + by rewrite -[7]/(2 + (3 +2)) (eqn_add2r) -{2} v0 => /eqP/DUR_injv. + by rewrite addnA addn1 eqSS => /(Hj _ (leqnn 4)). + by rewrite -[7]/(4 + (1 +2)) (eqn_add2r) => ha; move: Hf; rewrite ha. + by rewrite -[7]/(3 + (3 +1)) (eqn_add2r) -{2} v2 => /eqP/DUR_injv. + by rewrite -[7]/(2 + (3 +2)) (eqn_add2r) -{2} v0 => /eqP/DUR_injv. + by rewrite addnA addn1 eqSS => /(Hj _ (ltnW (leqnn 5))). rewrite !spec_sorted_rec /spec_sorted /= ! andbT. rewrite /Zval_v !big_cons big_nil addn0 leqn1. case/andP; case/orP => /eqP sa; case/orP => /eqP sb; rewrite sa sb ? v0 ? v1 ? v2 // => /eqP; rewrite addn1 eqSS => /eqP v3. clear a7 b7 sa sb. move:(v_exists 8) => [l]. case:l; [by rewrite Hd | move => a8]; case. by move/He => h1 h2; move: h1; rewrite h2. move => b8; case. rewrite !spec_sorted_rec /spec_sorted /= ! andbT. rewrite /Zval_v !big_cons big_nil addn0 leqn1. case/andP; case/orP => /eqP sa; case/orP => /eqP sb; rewrite sa sb ? v0 ? v1 ? v2 // => /eqP; rewrite addn1 eqSS v3 //. move => c8; case; last by move => a l /Hi => h1 h2; move: h1; rewrite h2. rewrite !spec_sorted_rec /spec_sorted /= ! andbT. rewrite /Zval_v !big_cons big_nil addn0 leqn1. case/and3P; case/orP => /eqP ea; case/orP => /eqP eb; case/orP => /eqP ec; rewrite ea eb ec ?v0 ?v1 ?v2 ?v3 => /eqP //. + by rewrite -[8]/(1 + (6 +1)) (eqn_add2r) -{2} v1 => /eqP/DUR_injv. + rewrite -[8]/(4 + (3 +1)) (eqn_add2r) => /eqP v4. by move:(DUR_exclusion2 1); rewrite v1 v2 v3 v4. + by rewrite -[8]/(3 + (3 +2)) (eqn_add2r) -{2} v2 => /eqP/DUR_injv. + by rewrite -[8]/(1 + (6 +1)) (eqn_add2r) -{2} v1 => /eqP/DUR_injv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)