proposition: Lemma Rle_dec_weak:forall (x y:R), {Rle x y}+{(Rle y x)}.
proof: Proof. intros x y; case (Rlt_le_dec x y); intros; [ left | right ]; trivial; apply Rlt_le; trivial. Defined.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)