proposition: Lemma Rtotal_order : forall r1 r2, 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; left. - now right; right. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField