proposition: Lemma Rlt_dichotomy_converse : forall r1 r2, r1 < r2 \/ r1 > r2 -> r1 <> r2.
proof: Proof. intros r1 r2 [Hlt | Hgt]. - now apply Rlt_not_eq. - now apply Rgt_not_eq. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField