proposition: Theorem binomial_expansion : ∀ (a : α) n, (lap_power [a; 1%K … []] n = List.map (nth_coeff a n) (List.seq 0 (S n)))%lap.
proof: Proof. intros a n. induction n. simpl. unfold nth_coeff; simpl. rewrite rng_add_0_l. reflexivity. remember List.seq as f; simpl; subst f. rewrite IHn. remember (List.map (nth_coeff a (S n)) (List.seq 0 (S (S n)))) as r. rewrite lap_mul_cons_l. rewrite lap_mul_1_l. rewrite lap_mul_const_l. rewrite List.map_map. rewrite List_seq_split_first in |- * at 1. remember (S n) as s; simpl. unfold nth_coeff at 1; simpl. rewrite comb_0_r, Nat.sub_0_r, rng_add_0_r. rewrite rng_mul_nat_1_l. subst s. rewrite List_seq_split_last. rewrite Nat.add_0_l. rewrite <- List.seq_shift. rewrite List.map_map. rewrite List.map_app; simpl. rewrite lap_app_add, lap_add_assoc. rewrite List.map_length, List.seq_length. unfold nth_coeff at 3. rewrite comb_id, Nat.sub_diag; simpl. rewrite lap_add_map2. unfold nth_coeff; simpl. subst r. remember (S n) as sn; simpl; subst sn. constructor. unfold nth_coeff; simpl. rewrite rng_add_0_l; reflexivity. rewrite List_seq_split_last. simpl. rewrite List.map_app. simpl. rewrite lap_app_add. rewrite List.map_length. rewrite List.seq_length. unfold nth_coeff at 2. rewrite Nat.sub_diag. rewrite comb_id. apply lap_add_compat; [ idtac | destruct n; reflexivity ]. rewrite <- List.seq_shift. rewrite List.map_map. apply lap_eq_map_ext. intros b. unfold nth_coeff; simpl. rewrite <- rng_mul_nat_mul_swap. rewrite rng_mul_nat_add_distr_r. rewrite rng_add_comm. apply rng_add_compat_l. destruct (eq_nat_dec n b) as [H₁| H₁]. subst b; simpl. rewrite comb_lt; [ | apply Nat.lt_succ_diag_r ]. reflexivity. destruct (le_dec (S b) n) as [H₂| H₂]. rewrite Nat.sub_succ_r. remember (n - b)%nat as nb eqn:Hnb . symmetry in Hnb. destruct nb; [ simpl | reflexivity ]. apply Nat.sub_0_le in Hnb. apply Nat.nle_gt in H₂; contradiction. apply Nat.nle_gt in H₂. rewrite comb_lt; [ reflexivity | assumption ]. Qed.
imports: Utf8 QArith NPeano Sorting Misc SlopeMisc Slope_base QbarM NbarM Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull PolyConvexHull NotInSegment Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq PosOrder F1Prop InK1m Q_field RootHeadTail