proposition: Theorem list_div_x_sub_c_ne_0 : ∀ la c r len, not (lap_eq la []) → list_root_multiplicity acf c la len = r → length la ≤ len → (apply_lap (list_quotient_phi_x_sub_c_pow_r R la c r) c ≠ 0)%K.
proof: Proof. intros la c r len Hla Hmult Hlen. revert la len Hla Hmult Hlen. induction r; intros; simpl. intros Happ; apply Hla; clear Hla. revert la Hmult Hlen Happ. induction len; intros. destruct la; [ idtac | exfalso; revert Hlen; apply Nat.nle_succ_0 ]. reflexivity. destruct la as [| a]; [ reflexivity | idtac ]. simpl in Hmult. unfold lap_mod_deg_1 in Hmult; simpl in Hmult. simpl in Hlen. apply le_S_n in Hlen. simpl in Happ. destruct (fld_zerop (apply_lap la c * c + a)%K). discriminate Hmult. contradiction. destruct len. destruct la; [ idtac | exfalso; revert Hlen; apply Nat.nle_succ_0 ]. exfalso; apply Hla; reflexivity. simpl in Hmult. destruct (fld_zerop (lap_mod_deg_1 la c)) as [Hz| Hnz]. apply eq_add_S in Hmult. destruct la as [| a]; [ exfalso; apply Hla; reflexivity | idtac ]. simpl in Hlen. apply le_S_n in Hlen. eapply IHr. intros H; apply Hla; clear Hla. unfold lap_div_deg_1 in H; simpl in H. unfold lap_mod_deg_1 in Hz; simpl in Hz. remember (lap_mod_div_deg_1 R la c) as md eqn:Hmd . symmetry in Hmd. assert (apply_lap la c = 0)%K as Happ. apply lap_mod_deg_1_apply. unfold lap_mod_deg_1; simpl. rewrite Hmd. destruct md as [| d]; [ reflexivity | idtac ]. apply lap_eq_cons_nil_inv in H. destruct H; assumption. rewrite Happ in Hz. rewrite rng_mul_0_l, rng_add_0_l in Hz. constructor; [ assumption | idtac ]. destruct len. destruct la; [ idtac | exfalso; revert Hlen; apply Nat.nle_succ_0 ]. reflexivity. simpl in Hmult. unfold lap_div_deg_1 in Hmult; simpl in Hmult. revert Hmd H; clear; intros. revert md Hmd H. induction la as [| a]; intros; [ reflexivity | simpl ]. constructor. simpl in Hmd. subst md. apply lap_eq_cons_nil_inv in H. destruct H as (Happ, H). assert (apply_lap la c = 0)%K as Haz. apply lap_mod_deg_1_apply. unfold lap_mod_deg_1. remember (lap_mod_div_deg_1 R la c) as md eqn:Hmd . symmetry in Hmd. destruct md as [| m]; [ reflexivity | idtac ]. apply lap_eq_cons_nil_inv in H. destruct H; assumption. rewrite Haz, rng_mul_0_l, rng_add_0_l in Happ. assumption. simpl in Hmd. subst md. apply lap_eq_cons_nil_inv in H. destruct H as (Happ, H). eapply IHla; [ reflexivity | eassumption ]. eassumption. unfold lap_div_deg_1; simpl. revert Hlen; clear; intros. revert len Hlen. induction la as [| a]; intros; [ apply Nat.le_0_l | simpl ]. destruct len; [ exfalso; revert Hlen; apply Nat.nle_succ_0 | simpl ]. simpl in Hlen. apply le_S_n in Hlen. apply le_n_S, IHla; assumption. discriminate Hmult. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn