proposition: Theorem nth_char_lap_eq_coeff : ∀ i j li la, (j + i)%nat ∈ li → Sorted Nat.lt li → (∀ m : nat, m ∈ li → j ≤ m) → (List.nth i (make_char_lap_of_hl la j li) 0 = coeff_of_hl la (j + i) li)%K.
proof: Proof. intros i j li la Hjil Hs Hm. revert i j Hjil Hm. induction li as [| n]; intros; simpl; [ now rewrite match_id | ]. destruct Hjil as [H| H]. subst n. rewrite Nat.add_comm, Nat.add_sub; simpl. rewrite list_nth_pad_sub, Nat.sub_diag; simpl; [ | easy ]. remember (i + j)%nat as n eqn:Hn . destruct (eq_nat_dec n n) as [H| H]; [ reflexivity | idtac ]. exfalso; apply H; reflexivity. destruct (eq_nat_dec (j + i) n) as [H₁| H₁]. rewrite list_nth_pad_sub. rewrite <- H₁. rewrite Nat.add_comm, Nat.add_sub; simpl. rewrite Nat.sub_diag; reflexivity. rewrite <- H₁, Nat.add_sub_swap; auto with Arith. rewrite Nat.sub_diag; reflexivity. assert (n ≤ j + i)%nat as Hnij. apply Nat.lt_le_incl. apply Sorted_StronglySorted in Hs. specialize (StronglySorted_inv Hs) as (_, Hss). rewrite List.Forall_forall in Hss. now apply Hss. now intros x y z Hxy Hyz; transitivity y. rewrite list_nth_pad_sub. remember (i - (n - j))%nat as p eqn:Hp . symmetry in Hp. destruct p; simpl. rewrite Nat.add_comm in Hnij. assert (Hjn : j ≤ n); [ apply Hm; left; reflexivity | exfalso ]. apply H₁; symmetry. rewrite Nat.add_comm. apply Nat.le_antisymm; auto with Arith. apply Nat.sub_0_le. rewrite <- Nat_sub_sub_distr; auto with Arith. apply Nat.add_sub_eq_nz in Hp; [ idtac | intros H₂; discriminate H₂ ]. assert (Hjn: j ≤ n) by (apply Hm; left; reflexivity). rewrite <- Nat.add_sub_swap in Hp; auto with Arith. apply Nat.add_cancel_r with (p := j) in Hp. eapply Nat.add_le_mono in Hjn; [ idtac | apply Nat.le_0_l ]. rewrite Nat.add_0_l, Nat.add_comm in Hjn. rewrite Nat.sub_add in Hp; eauto . rewrite Nat.add_succ_r, <- Nat.add_succ_l in Hp. rewrite <- Nat.add_comm, <- Hp. rewrite IHli; auto with Arith. eapply Sorted_inv; eassumption. rewrite Hp, Nat.add_comm; assumption. intros q Hq. apply Sorted_StronglySorted in Hs. specialize (StronglySorted_inv Hs) as (_, Hss). rewrite List.Forall_forall in Hss. now apply Hss. now intros x y z Hxy Hyz; transitivity y. apply Nat.sub_le_mono_r with (p := j) in Hnij. rewrite Nat.add_comm, Nat.add_sub in Hnij; assumption. Qed.
imports: Utf8 QArith NPeano Sorted ConvexHullMisc ConvexHull PolyConvexHull Field2 Misc Newton NbarM QbarM SplitList Fsummation Fpolynomial Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base CharactPolyn AlgCloCharPol