proposition: Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3.
proof: Proof. intros r1 r2 r3 H1%Rge_le H2%Rge_le. now apply Rle_ge, (Rle_trans _ r2). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField