proposition: Lemma Req_dec_T : forall r1 r2:R, {r1 = r2} + {r1 <> r2}.
proof: Proof. intros r1 r2; destruct (total_order_T r1 r2) as [[H | ] | H]. - now right; intros ->; apply (Rlt_irrefl r2). - now left. - now right; intros ->; apply (Rlt_irrefl r2 H). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField