I want to prove the following theorem in Coq.
Please give me an advice if possible.
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.