proposition: Lemma gauss_lemma : forall p q, gcdsr (p * q) %= gcdsr p * gcdsr q.
proof: Proof. apply: @poly_ind2=> [p|q|p0 p1 q0 q1]; first by rewrite mulr0 !gcdsr0 mulr0. by rewrite mul0r !gcdsr0 mul0r. set p := p1 * 'X + p0%:P. set q := q1 * 'X + q0%:P. move=> IH1 IH2. case: (gcdsr_primitive p); rewrite /primitive=> p' [Hp prim_p']. case: (gcdsr_primitive q); rewrite /primitive=> q' [Hq prim_q']. case: (elim_poly p')=> p1' [p0'] Hp'. case: (elim_poly q')=> q1' [q0'] Hq'. case H0p0 : (p0 == 0). rewrite /p (eqP H0p0) addr0 -mulrA ['X * _]mulrC mulrA. rewrite (eqd_trans (gcdsr_mulX _)) // (eqd_trans IH1) //. by rewrite eqd_sym (eqd_mul (gcdsr_mulX _)). case H0q0 : (q0 == 0). rewrite /q (eqP H0q0) addr0 mulrA (eqd_trans (gcdsr_mulX _)) //. by rewrite (eqd_trans IH2) // eqd_sym (eqd_mul _ (gcdsr_mulX _)). have Hp1p1' : p1 = (gcdsr p)%:P * p1'. apply/polyP=> i; move: Hp; rewrite {1}/p Hp' mulrDr mulrA -polyCM. move/polyP=> H; move: (H (i.+1)); rewrite -!cons_poly_def !coef_cons. by case i. have Hq1q1' : q1 = (gcdsr q)%:P * q1'. apply/polyP=> i; move: Hq; rewrite {1}/q Hq' mulrDr mulrA -polyCM. move/polyP=> H; move: (H (i.+1)); rewrite -!cons_poly_def !coef_cons. by case i. have Hgcdsrp0 : (gcdsr p != 0) by rewrite /p gcdsr_gcdl gcdr_eq0 H0p0. have Hgcdsrq0 : (gcdsr q != 0) by rewrite /q gcdsr_gcdl gcdr_eq0 H0q0. have IH1' : gcdsr (p1' * q') %= gcdsr p1'. rewrite -(@eqd_mul2r _ (gcdsr q)) ?(eqd_trans (mulr_gcdsl _ _)) // -mulrA. rewrite [q' * _]mulrC -Hq -(@eqd_mul2l _ (gcdsr p)) // mulrA. rewrite (eqd_trans (mulr_gcdsr _ _)) // mulrA -Hp1p1' eqd_sym. by rewrite (eqd_trans (eqd_mul (mulr_gcdsr _ _) (eqdd _))) // -Hp1p1' eqd_sym. have IH2' : gcdsr (p' * q1') %= gcdsr q1'. rewrite -(@eqd_mul2l _ (gcdsr p)) ?(eqd_trans (mulr_gcdsr _ _)) // mulrA. rewrite -Hp -(@eqd_mul2r _ (gcdsr q)) // (eqd_trans (mulr_gcdsl _ _)) //. rewrite -!mulrA [q1' * _]mulrC -Hq1q1' eqd_sym mulrC [gcdsr q1' * _]mulrC. by rewrite (eqd_trans (eqd_mul (mulr_gcdsr _ _) (eqdd _))) // -Hq1q1' mulrC eqd_sym. suff Hprim : (gcdsr (p' * q') %= 1). rewrite {1}Hp {1}Hq mulrAC mulrA -polyCM-mulrA. rewrite (eqd_trans (gcdsr_mull _ _)) // [q' * _]mulrC -{2}[gcdsr q]mulr1. rewrite mulrA (eqd_mul _ _) //. rewrite Hp' Hq' mulrC. rewrite mulrDr !mulrDl -polyCM mulrCA [_ * p0'%:P]mulrC !mulrA. rewrite !addrA -mulrDl -mulrDl. rewrite gcdsr_gcdl -/(coprimer _ _) coprimer_mull andbC /coprimer {1}addrC. rewrite [_ + q0'%:P * p1']addrC -addrA (eqd_trans (gcdr_gcdsr_muladdr _ _ _)). rewrite (eqd_trans (gcdr_gcdsr_muladdr _ _ _)) // -mulrA [_ * 'X]mulrC mulrA. rewrite -mulrDl -Hp' (eqd_trans (eqd_gcd (eqdd _) IH2')) // -gcdsr_gcdl. by rewrite -Hq'. rewrite [_ * p1']mulrC -mulrA -mulrDr addrC -Hq'. by rewrite (eqd_trans (eqd_gcd (eqdd _) IH1')) // -gcdsr_gcdl -Hp'. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset ssralg) mathcomp(matrix poly) mathcomp(bigop polydiv) CoqEAL(stronglydiscrete dvdring)