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