I make the following code, and I'm in stuck. Please help me.
From mathcomp Require Import all_ssreflect.
Require Import QArith.
Lemma Qle_total (x : Q) (y : Q) :
x <= y \/ not (x <= y).
Proof.
How to prove "$x \le y$" or "not $(x \le y)$" for rational numbers $x$ and $y$ in Coq?
with-forest
- 387
- 1
- 8