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