proposition: Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> ~ r1 < r2.
proof: Proof. intros r1 r2 [Hlt | Heq%eq_sym]; intros Hgt. - now apply (Rlt_asym r1 r2). - now apply Rlt_not_eq in Hgt. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField