proposition: Lemma Rle_trans : forall r1 r2 r3, r1 <= r2 -> r2 <= r3 -> r1 <= r3.
proof: Proof. intros r1 r2 r3 [Hlt | ->]; try easy. intros [Hlt' | ->]. - now left; apply (Rlt_trans _ r2). - now left. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField