proposition: Lemma Rle_lt_or_eq : forall r1 r2, r1 <= r2 -> r1 < r2 \/ r1 = r2.
proof: Proof. now intros r1 r2 H; apply Private_sumbool_to_or, Rle_lt_or_eq_dec. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField