proposition: Lemma unicity_decomposition (s1 s2 : seq {poly R}) : forall (p : {poly R}), (forall r, r \in s1 -> irreducible_poly r) -> (forall r, r \in s2 -> irreducible_poly r) -> (forall r, r \in s1 -> r \is monic) -> (forall r, r \in s2 -> r \is monic) -> p = \prod_(r <- s1) r -> p = \prod_(r <- s2) r -> perm_eq s1 s2.
proof: Proof. elim: s1 s2=> [|a1 l1 IHl s2 p Irr1 Irr2 mon1 mon2]. case=> // a l p _ Irr2 _ mon2->. rewrite big_nil big_cons=> eq1M. have: irreducible_poly a by apply: Irr2; rewrite mem_head. rewrite /irreducible_poly; case. by rewrite ltnNge leq_eqVlt -dvdp1 eq1M dvdp_mulr. rewrite big_cons=> eqpM eqpbig /=. have a1ins2: a1 \in s2. apply: (irreducible_dvdp_seq _ _ _ Irr2 mon2 eqpbig). + by apply: Irr1; rewrite mem_head. - by rewrite mon1 // mem_head. by rewrite eqpM dvdp_mulr. rewrite perm_sym (perm_trans (perm_to_rem a1ins2)) //. rewrite perm_cons perm_sym. have nza1: a1 != 0. by apply: irredp_neq0; apply: Irr1; rewrite mem_head. rewrite (perm_big _ (perm_to_rem a1ins2)) /= big_cons eqpM in eqpbig. have/(mulfI nza1) eqbig := eqpbig. set q:= \prod_(j <- l1) j. apply: (IHl _ q)=> // r Hr. + by apply: Irr1; rewrite mem_behead. - by apply: Irr2; rewrite (mem_rem Hr). + by rewrite mon1 // mem_behead. - by rewrite mon2 // (mem_rem Hr). Qed.
imports: mathcomp(all_ssreflect all_algebra)