proposition: Lemma Rle_dec : forall r1 r2, {r1 <= r2} + {~ r1 <= r2}.
proof: Proof. intros r1 r2; destruct (Rlt_dec r2 r1) as [H%Rlt_not_le | H%Rnot_lt_le]. - now right. - now left. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField