proposition: Lemma Rnot_lt_le : forall r1 r2, ~ r1 < r2 -> r2 <= r1.
proof: Proof. intros r1 r2 H; destruct (Rtotal_order r1 r2) as [Hlt | [Heq | Hgt]]. - now exfalso. - now right. - now left. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField