proposition: Lemma cpoly_div2 : forall (n m : nat) (a b c : cpoly_cring CR), degree_le n a -> monic m b -> degree_lt_pair c b -> a [*] b [=] c -> a [=] [0].
proof: Proof. induction n. intros m a b c H X H1 H2; destruct (degree_le_zero _ _ H) as [x s]. revert H1. rewrite -> s; destruct X as [H0 H1]; rewrite -> c_zero. rewrite -> s in H2. intro. apply cpoly_const_eq. destruct m. generalize (nth_coeff_wd _ 0 _ _ H2); destruct H3 as [d s0]. rewrite -> nth_coeff_c_mult_p, H0, mult_one, (nth_coeff_wd _ _ _ _ (s0 H1)). intro tmp; apply tmp. generalize (nth_coeff_wd _ (S m) _ _ H2); destruct H3 as [d s0]. rewrite -> nth_coeff_c_mult_p, H0, mult_one, (d m H1 (S m)). intro; assumption. apply le_n. intros. induction a as [ | a s ] using cpoly_induc; [ reflexivity | ]. apply _linear_eq_zero. revert H2. rewrite -> cpoly_lin, ring_distl_unfolded. intro H2. cut (a [=] [0]); [ intro aeqz; split; [ | apply aeqz ] | ]. assert (s [=] nth_coeff m (_C_ s[*]b[+]_X_[*]a[*]b)). destruct H0; rewrite -> nth_coeff_plus, nth_coeff_c_mult_p, H0. rewrite -> (nth_coeff_wd _ _ _ [0]); [ simpl; ring | ]. rewrite -> aeqz; ring. rewrite -> H3. rewrite -> (nth_coeff_wd _ _ _ _ H2). destruct H1 as [d s0]. destruct H0 as [H0 H1]. destruct m; [ rewrite -> (nth_coeff_wd _ _ _ _ (s0 H1)); reflexivity | apply (d m H1); apply le_n ]. apply (IHn (S m) _ ([0] [+X*] b) (c [-] _C_ s [*] b)); [ | | | rewrite <- H2, cpoly_lin, <- c_zero; unfold cg_minus; ring ]. unfold degree_le; intros; rewrite <- (coeff_Sm_lin _ _ s). apply H; apply -> Nat.succ_lt_mono; apply H3. split; [ rewrite -> coeff_Sm_lin; destruct H0; apply H0 | unfold degree_le; intros ]. destruct m0; [ inversion H3 | simpl; destruct H0 ]. apply H4; apply Nat.succ_lt_mono; apply H3. unfold degree_lt_pair. split; intros. unfold degree_le; intros. rewrite -> nth_coeff_minus, nth_coeff_c_mult_p, (degree_le_cpoly_linear _ _ _ _ H3); [ | apply H4 ]. rewrite -> cring_mult_zero, cg_inv_zero; destruct H1 as [d s0]. destruct m; [ destruct H0; apply (nth_coeff_wd _ _ _ _ (s0 H1)) | ]. apply (d n0); [ | apply H4 ]. apply (degree_le_mon _ _ n0); [ apply le_S; apply le_n | apply (degree_le_cpoly_linear _ _ _ _ H3) ]. destruct (degree_le_zero _ _ H3) as [x s0]. revert s0. rewrite -> cpoly_C_. intro s0. destruct (linear_eq_linear_ _ _ _ _ _ s0) as [H4 H5]. rewrite <- H2, -> H5. unfold cg_minus. ring. Qed.
imports: CPoly_Degree Lia