proposition: Lemma R_of_Q_le x y : Qle_bool x y = (R_of_Q x <= R_of_Q y :> F).
proof: Proof. rewrite /Qle_bool /R_of_Q /=. rewrite ler_pdivrMr ?ltr0n; last lia. rewrite mulrAC ler_pdivlMr ?ltr0n; last lia. rewrite !pmulrn -!intrM ler_int; lia. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)