proposition: Lemma Rminus_lt : forall r1 r2, r1 - r2 < 0 -> r1 < r2.
proof: Proof. unfold Rminus; intros r1 r2 H. now apply (Rplus_lt_reg_r (-r2)); rewrite Rplus_opp_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField