proposition: Lemma Rdichotomy : forall r1 r2, r1 <> r2 -> r1 < r2 \/ r1 > r2.
proof: Proof. intros r1 r2 r1_neq_r2; destruct (Rtotal_order r1 r2) as [Hlt | [Heq | Hgt]]. - now left. - now exfalso. - now right. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField