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