proposition: Lemma fracqE x : fracq x = x.1%:Q / x.2%:Q.
proof: Proof. move: x => [m n] /=; apply/val_inj; rewrite val_fracq/=. case: eqVneq => //= [->|n_neq0]; first by rewrite rat0 invr0 mulr0. rewrite -[m%:Q]valqK -[n%:Q]valqK. rewrite [_^-1]invq_frac ?denq_neq0 ?numq_eq0 ?intq_eq0//=. rewrite [X in valq X]mulq_frac val_fracq /invq_subdef !mulq_subdefE/=. by rewrite -!/(numq _) -!/(denq _) !numq_int !denq_int mul1r mulr1 n_neq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)