proposition: Lemma Rle_lt_or_eq_dec : forall r1 r2, r1 <= r2 -> {r1 < r2} + {r1 = r2}.
proof: Proof. intros r1 r2 H; destruct (total_order_T r1 r2) as [[Hlt | Heq] | Hgt]. - now left. - now right. - now exfalso; apply (Rgt_not_le r1 r2). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField