proposition: Theorem length_list_quotient_phi_x_sub_c_pow_r : ∀ l c r, length (list_quotient_phi_x_sub_c_pow_r R l c r) = (length l - r)%nat.
proof: Proof. intros l c r. revert l c. induction r; intros; simpl. rewrite Nat.sub_0_r; reflexivity. destruct l as [| x]; simpl. unfold lap_div_deg_1; simpl. rewrite IHr; reflexivity. unfold lap_div_deg_1; simpl. rewrite IHr. rewrite length_lap_mod_div_deg_1; reflexivity. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn