# How to Deal with Qle_bool in the progress of proving in Coq

I want to prove the following theorem in Coq.

From mathcomp Require Import all_ssreflect.

Require Import QArith.

Theorem Compare_rationals (q1 : Q) (q2 : Q) :
(if Qle_bool q1 q2 then 1 else 0) == 0 \/
(if Qle_bool q1 q2 then 1 else 0) == 1.
Proof.


You may do a case analysis on Qle_bool q1 q2:
Proof. by case (Qle_bool q1 q2) ; [right | left]. Qed.