proposition: Theorem find_coeff_add : ∀ f L m mx p dp i, (find_coeff mx (p + dp) m f L (i + dp) = find_coeff mx p m f L i)%K.
proof: Proof. intros f L m mx p dp i. revert f L m p dp i. induction mx; intros; [ reflexivity | simpl ]. destruct (ps_zerop K (ps_poly_nth 0 f)) as [| H₁]; [ reflexivity | ]. rewrite <- Nat_compare_add. remember (Nat.compare p i) as cmp eqn:Hcmp . symmetry in Hcmp. destruct cmp; [ reflexivity | | reflexivity ]. rewrite next_pow_add. apply IHmx. Qed.
imports: Utf8 QArith NPeano Sorting Misc Field2 Fpolynomial Fsummation Newton ConvexHull Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq F1Prop Q_field PosOrder QbarM