proposition: Lemma R_of_Q_eq x y : Qeq_bool x y = (R_of_Q x == R_of_Q y :> F).
proof: Proof. rewrite /Qeq_bool /R_of_Q /= eqr_div ?pnatr_eq0; try lia. rewrite !pmulrn -!intrM eqr_int -!/(int_of_Z (Z.pos _)) -!rmorphM /=. by rewrite (can_eq int_of_ZK); apply/idP/eqP => /Zeq_is_eq_bool. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)