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