proposition: Lemma Rge_ge_eq : forall r1 r2, r1 >= r2 /\ r2 >= r1 <-> r1 = r2.
proof: Proof. intros r1 r2; split. - now intros [H1 H2]; apply Rge_antisym. - now intros ->; split; apply Rge_refl. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField