proposition: Theorem cpoly_div1 : forall (m n : nat) (f g : cpoly_cring CR), degree_le m f -> degree_le (S n) g -> n <= m -> {qr: (cpoly_cring CR)*(cpoly_cring CR) & let (q,r):=qr in f [*] _C_ ((nth_coeff (S n) g) [^] (m - n)) [=] q [*] g [+] r & let (q,r):=qr in degree_le n r}.
proof: Proof. intros m n; generalize (refl_equal (m - n)). generalize (m - n) at 1 as p; intro p; revert m n; induction p; intros. exists (([0] : cpoly_cring CR),f). rewrite <- H. simpl (nth_coeff (S n) g[^]0). rewrite <- c_one. ring. replace n with m by lia; assumption. set (f1 := (_C_ (nth_coeff (S n) g) [*] f [-] _C_ (nth_coeff m f) [*] ((_X_ [^] (m - (S n))) [*] g))). destruct (IHp (m - 1) n) with (f := f1) (g := g); [ lia | | assumption | lia | ]. unfold f1; clear f1. assert (HypTmp : m = S (m - 1)); [ lia | rewrite HypTmp; rewrite <- HypTmp at 1 ]. apply degree_poly_div; [ lia | rewrite <- HypTmp; assumption | assumption ]. destruct x as [q1 r1]. exists (q1 [+] _C_ ((nth_coeff (S n) g)[^](m - S n) [*] (nth_coeff m f)) [*] _X_ [^] (m - S n), r1); [ | assumption]. unfold f1 in y. rewrite -> ring_distl_unfolded. rewrite <- plus_assoc_unfolded. rewrite -> (cag_commutes _ _ r1). rewrite -> plus_assoc_unfolded. rewrite <- y. replace (m - n) with (S (m - S n)) by lia. replace (m - 1 - n) with (m - S n) by lia. rewrite <- nexp_Sn. generalize (nth_coeff (S n) g) (nth_coeff m f) (m - S n). intros. rewrite c_mult, c_mult. unfold cg_minus. ring. Qed.
imports: CPoly_Degree Lia