proposition: Lemma freegequivP s1 s2 (hs1 : reduced s1) (hs2 : reduced s2) : reflect (precoeff^~ s1 =1 precoeff^~ s2) (fgequiv (mkPrefreeg s1 hs1) (mkPrefreeg s2 hs2)).
proof: Proof. apply: (iffP idP); rewrite /fgequiv /=. by move=> H k; apply: precoeff_perm_eq. move=> H; apply: uniq_perm. - by move/reduced_uniq/map_uniq: hs1. - by move/reduced_uniq/map_uniq: hs2. by move=> [z k]; rewrite !reduced_mem // H. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)