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