proposition: Lemma Rgt_minus_pos : forall r1 r2, 0 < r2 -> r1 > r1 - r2.
proof: Proof. intros r1 r2 H%Ropp_lt_contravar; rewrite Ropp_0 in H. now rewrite <-(Rplus_0_r r1) at 1; apply (Rplus_lt_compat_l r1). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField