proposition: Lemma cpoly_div : forall (f g : cpoly_cring CR) (n : nat), monic n g -> ex_unq (fun (qr : ProdCSetoid (cpoly_cring CR) (cpoly_cring CR)) => f[=](fst qr)[*]g[+](snd qr) and degree_lt_pair (snd qr) g).
proof: Proof. intros f g n H; destruct n. destruct H; destruct (degree_le_zero _ _ H0). rewrite -> (nth_coeff_wd _ _ _ _ s) in H. simpl in H; rewrite -> H in s. exists (f,[0]). intros; destruct y; simpl (snd (s0, s1)) in *; simpl (fst (s0, s1)) in *. rename H1 into X. destruct X; destruct d; split; [ | symmetry; apply (s3 H0) ]. rewrite -> s2, (s3 H0), s, <- c_one; ring. simpl (fst (f, [0] : cpoly_cring CR)); simpl (snd (f, [0] : cpoly_cring CR)). replace (cpoly_zero CR) with ([0] : cpoly_cring CR) by (simpl;reflexivity). split; [ rewrite -> s, <- c_one; ring | ]. split; [ | reflexivity ]. unfold degree_le; intros; apply nth_coeff_zero. destruct (@cpoly_div1 (Nat.max (lth_of_poly f) n) n f g); [ | destruct H; assumption | apply Nat.le_max_r | ]. apply (@degree_le_mon _ _ (lth_of_poly f)); [ apply Nat.le_max_l | apply poly_degree_lth ]. destruct H; destruct x as [q r]. rewrite -> H, one_nexp, mult_one in y. assert (f[=]q[*]g[+]r and degree_lt_pair r g). split; [ assumption | ]. split. intros; unfold degree_le; intros; apply y0; apply Nat.le_lt_trans with n0; [ | assumption ]. unfold degree_le in H1; apply not_gt; intro; unfold gt in H3. set (tmp := (H1 (S n) (proj1 (Nat.succ_lt_mono _ _) H3))); rewrite -> H in tmp. apply (eq_imp_not_ap _ _ _ tmp); apply ring_non_triv. intro; unfold degree_le in H1; rewrite -> H1 in H; [ | apply Nat.lt_0_succ ]. destruct (eq_imp_not_ap _ _ _ H); apply ap_symmetric; apply ring_non_triv. exists (q,r); [ | assumption ]. intros y1 X0; destruct y1 as [q1 r1]; simpl (fst (q1, r1)); simpl (snd (q1, r1)) in X0. rename H1 into X. destruct X; destruct X0; rewrite -> s in s0; assert (q [=] q1). apply cg_inv_unique_2. apply (@cpoly_div2 (lth_of_poly (q [-] q1)) (S n) (q [-] q1) g (r1 [-] r)); [ apply poly_degree_lth | split; assumption | | ]. destruct d; destruct d0; split. intros; apply degree_le_minus; [ apply d0 | apply d ]; assumption. intro; rewrite -> (s1 H1) ,(s2 H1); unfold cg_minus; ring. assert (r1[=]q1[*]g[+]r1[-]q1[*]g); [ unfold cg_minus; ring | ]. rewrite -> H1, <- s0; unfold cg_minus; ring. split; [ assumption | ]. rewrite -> H1 in s0; apply (cg_cancel_lft _ _ _ _ s0). Qed.
imports: CPoly_Degree Lia