proposition: Theorem fold_nothing : ∀ A j len (f : _ → _ → A) g la, (∀ i, j ≤ i → (i < j + len)%nat → g i = false) → List.fold_right (λ i accu, if g i then f i accu else accu) la (List.seq j len) = la.
proof: Proof. intros A j len f g la Hg. revert j la Hg. induction len; intros; [ reflexivity | simpl ]. unfold lt in Hg; rewrite Nat.add_succ_r in Hg. rewrite Hg; [ idtac | reflexivity | apply le_n_S, le_plus_l ]. apply IHlen. intros i Hji Hij. apply Hg; [ idtac | assumption ]. apply le_Sn_le; 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