proposition: Theorem Rlt_Rminus_ZERO : forall r1 r2 : R, (r2 < r1)%R -> (0 < r1 - r2)%R.
proof: Proof. intros r1 r2 H; replace 0%R with (r1 - r1)%R; unfold Rminus in |- *; auto with real. Qed.
imports: Coq(ZArith Classical_Prop) Coq(Rbase Rfunctions Ranalysis Rtrigo)