proposition: Lemma pi_is_multiplicative : multiplicative \pi_Q.
proof: Proof. by split; do ?move=> x y /=; rewrite !piE. Qed.
imports: HB(structures) mathcomp(ssreflect eqtype choice ssreflect ssrbool ssrnat) mathcomp(ssrfun seq ssralg generic_quotient)