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