proposition: Lemma degree_poly_div : forall (m n : nat) (f g : cpoly CR), let f1 := (_C_ (nth_coeff n g) [*] f [-] _C_ (nth_coeff (S m) f) [*] ((_X_ [^] ((S m) - n)) [*] g)) in S m >= n -> degree_le (S m) f -> degree_le n g -> degree_le m f1.
proof: Proof. intros m n f g f1 ge_m_n df dg p Hp; unfold f1; clear f1. rewrite -> nth_coeff_minus, nth_coeff_c_mult_p, nth_coeff_c_mult_p, nth_coeff_mult. rewrite -> (Sum_term _ _ _ (S m - n)); [ | lia | lia | intros ]. rewrite -> nth_coeff_nexp_eq. destruct Hp. replace (S m - (S m - n)) with n by lia. unfold cg_minus. ring. rewrite -> (dg (S m0 - (S m - n))); [ | lia]. rewrite -> df; [ unfold cg_minus; ring | lia]. rewrite nth_coeff_nexp_neq. ring. assumption. Qed.
imports: CPoly_Degree Lia