fact: Definition qle (a b c d : Z) (p : Qpositive) (a' b' c' d' : Z) (p' : Qpositive) : Prop := qlt a b c d p a' b' c' d' p' \/ a = a' /\ b = b' /\ c = c' /\ d = d' /\ p = p'.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)