proposition: Lemma Rle_gt_dec : forall r1 r2, {r1 <= r2} + {r1 > r2}.
proof: Proof. intros r1 r2; destruct (Rle_lt_dec r1 r2) as [Hle | H%Rlt_gt]. - now left. - now right. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField