proposition: Lemma Rle_antisym : forall r1 r2, r1 <= r2 -> r2 <= r1 -> r1 = r2.
proof: Proof. intros r1 r2 [Hlt | Heq] [Hgt | Heq']; try easy. now exfalso; apply (Rlt_asym r1 r2). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField