proposition: Lemma BQprod_inv x y:ratp x -> ratp y -> BQinv (x *q y) = BQinv x *q BQinv y.
proof: Proof. move => pa pb. have pc :=QS_inv pa. have pd :=QS_inv pb. case: (equal_or_not x \0q) => xz. rewrite xz BQinv_0 BQprod_0l // BQinv_0 BQprod_0l //. case: (equal_or_not y \0q) => yz. rewrite yz BQinv_0 BQprod_0r // BQinv_0 BQprod_0r //. symmetry; apply:BQ_inv_prop; try apply:QSp => //. rewrite BQprod_ACA // !BQprod_inv1 // BQprod_1l //; apply: QS1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)