proposition: Theorem fold_right_eqb_or : ∀ A j k len f (g : _ → A → A) la, (j < k)%nat → List.fold_right (λ i accu, if Nat.eqb i j || f i then g i accu else accu) la (List.seq k len) = List.fold_right (λ i accu, if f i then g i accu else accu) la (List.seq k len).
proof: Proof. intros A j k len f g la Hjk. revert j k Hjk. induction len; intros; [ reflexivity | simpl ]. rewrite IHlen. remember (Nat.eqb k j) as b eqn:Hb . symmetry in Hb. destruct b; [ idtac | reflexivity ]. apply Nat.eqb_eq in Hb. exfalso; subst k; revert Hjk; apply Nat.lt_irrefl. apply Nat.lt_lt_succ_r; 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