proposition: Lemma normal_changes : changes (seqn0 q) = 1%N.
proof: Proof. case : (ltngtP 3 (size (seqn0 q))) => Hsizeseqn0q. have Hincreasing1 := spseq_increasing; have Hincreasing2 := subspseq_increasing; have Hallpos := (subp_all_pos); have Hseqn0q := (seqn0_all_neq0 q); have Hseqn0spseq := (seqn0_all_neq0 spseq); have Hqsize := q_size; have Hqsize2 := p_size; have Hsizemidq := mid_seqn0q_size; have Hsizespseq := size_seqn0spseq_maskdropp; have Hqn1 := q_n_gt0; have Hqn2 := q_n_neq0; have Hq01 := q_0_lt0; have Hq02 := q_0_neq0. have H_1 : (0%N < (size (seqn0 q)).-1)%N. by rewrite -(ltn_add2r 1%N) !addn1 prednK (ltn_trans _ Hsizeseqn0q). have H_2 : (0%N < (size (seqn0 q)).-2)%N. by rewrite -(ltn_add2r 2) !addn2 prednK // prednK (ltn_trans _ Hsizeseqn0q). rewrite changes_decomp_sizegt2 //; last by rewrite (ltn_trans _ Hsizeseqn0q). rewrite mid_seqn0q_decomp changes_mult // seqn0_0 // seqn0q_1 //. rewrite {1}mid_seqn0q_decomp seqmul_coef. rewrite seqn0_n // seqn0q_n // {1}mid_seqn0q_decomp seqmul_coef. have H_3 : (0 < size (seqn0 spseq))%N. by rewrite -mid_seqn0q_size mid_size. have H_4 : (1 < size (seqn0 spseq))%N. by rewrite -mid_seqn0q_size mid_size -subn2 ltn_subRL addn1. case/orP : (changes_seq_incr Hincreasing2 Hseqn0spseq) => Hchanges. rewrite (eqP Hchanges). rewrite changes_seq_incr_1 // in Hchanges. move/andP : Hchanges => [] H0 H1. have H2: (q`_0 * ((seqn0 spseq)`_0 * (mask [seq x != 0 | x <- mid q] (drop 1 p))`_0) < 0) = false. apply: negbTE. rewrite -leNgt nmulr_rge0 // nmulr_rle0 // ltW //. apply/all_posP => //. by rewrite -Hsizespseq -Hsizemidq mid_size. rewrite H2 mid_seqn0q_size. have H3 : ((seqn0 spseq)`_(size (seqn0 spseq)).-1 * (mask [seq x != 0 | x <- mid q] (drop 1 p))`_ (size (seqn0 spseq)).-1 * q`_(size q).-1 < 0) = false. apply: negbTE. rewrite -leNgt mulrC pmulr_lge0 ?ltW // pmulr_lgt0 //. apply/all_posP => //. rewrite -Hsizespseq -Hsizemidq mid_size -{2}(subn2 (size (seqn0 q))) ltn_subRL addnC addn2 prednK // prednK //. by rewrite {2}(pred_Sn (size (seqn0 q))) -(subn1 (size (seqn0 q)).+1) ltn_subRL addnC addn1 prednK // (ltn_trans _ Hsizeseqn0q). by rewrite H3. rewrite (eqP Hchanges). rewrite changes_seq_incr_0 // in Hchanges. case : (ltrgtP 0 (seqn0 spseq)`_0) => Hspseqn0_0. have H1 : ((q`_0 * ((seqn0 spseq)`_0 * (mask [seq x != 0 | x <- mid q] (drop 1 p))`_0) < 0) = true). apply/eqP; rewrite eqb_id. rewrite nmulr_rlt0 // mulrC pmulr_lgt0 //. apply/all_posP => //. by rewrite -Hsizespseq -Hsizemidq mid_size. rewrite H1 mid_seqn0q_size. have H2 : (0 < (seqn0 spseq)`_(size (seqn0 spseq)).-1). by rewrite -(@pmulr_lgt0 _ (seqn0 spseq)`_0) // mulrC. have H3 : ((seqn0 spseq)`_(size (seqn0 spseq)).-1 * (mask [seq x != 0 | x <- mid q] (drop 1 p))`_ (size (seqn0 spseq)).-1 * q`_(size q).-1 < 0) = false. apply: negbTE. rewrite -leNgt mulrC pmulr_lge0 ?ltW // pmulr_lgt0 //. apply/all_posP => //. rewrite -Hsizespseq -Hsizemidq mid_size -{2}(subn2 (size (seqn0 q))) ltn_subRL addnC addn2 prednK // prednK //. by rewrite {2}(pred_Sn (size (seqn0 q))) -(subn1 (size (seqn0 q)).+1) ltn_subRL addnC addn1 prednK // (ltn_trans _ Hsizeseqn0q). by rewrite H3. have H1 : ((q`_0 * ((seqn0 spseq)`_0 * (mask [seq x != 0 | x <- mid q] (drop 1 p))`_0) < 0) = false). apply: negbTE. rewrite -leNgt nmulr_lge0 ?ltW // nmulr_rlt0 //. apply/all_posP => //. by rewrite -Hsizespseq -Hsizemidq mid_size. rewrite H1. have H2 : ((seqn0 spseq)`_(size (mid (seqn0 q))).-1 < 0). by rewrite Hsizemidq -(@nmulr_rgt0 _ (seqn0 spseq)`_0). have H3 : (((seqn0 spseq)`_(size (mid (seqn0 q))).-1 * (mask [seq x != 0 | x <- mid q] (drop 1 p))`_ (size (mid (seqn0 q))).-1 * q`_(size q).-1 < 0) = true). apply/eqP; rewrite eqb_id nmulr_rlt0 // nmulr_rlt0 //. apply/all_posP => //. rewrite -Hsizespseq -Hsizemidq mid_size -{2}(subn2 (size (seqn0 q))) ltn_subRL addnC addn2 prednK // prednK //. by rewrite {2}(pred_Sn (size (seqn0 q))) -(subn1 (size (seqn0 q)).+1) ltn_subRL addnC addn1 prednK // (ltn_trans _ Hsizeseqn0q). by rewrite H3. have := ((all_neq0P _ Hseqn0spseq) 0%N H_3). rewrite eq_sym => H_5. by have/eqP := H_5. by rewrite -Hsizespseq -Hsizemidq mid_size minnE subKn // -(ltn_add2r 3) !addn3 prednK. by rewrite -Hsizespseq -Hsizemidq minnE subKn // mid_size //. by rewrite -(ltn_add2r 1%N) !addn1 prednK // (ltn_trans _ Hsizeseqn0q). have Hsizeseqn0q2 : (size (seqn0 q) == 2%N). by rewrite eqn_leq -ltnS Hsizeseqn0q /= seqn0q_size. rewrite changes_decomp_size2 // ?seqn0_all_neq0 //. rewrite seqn0_0 ?q_0_neq0 // {1}(@pred_Sn 1) -(eqP Hsizeseqn0q2) seqn0_n ?q_n_neq0 //. apply/eqP. by rewrite eqb1 pmulr_llt0 ?q_0_lt0 // ?q_n_gt0. rewrite changes_size3 // ?seqn0_all_neq0 //. by rewrite seqn0_0 ?q_0_lt0 // q_0_neq0. by rewrite (@pred_Sn 2) Hsizeseqn0q seqn0_n ?q_n_gt0 // q_n_neq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)