proposition: Lemma Rmin_ge : forall a b c, c <= a -> c <= b -> c <= Rmin a b.
proof: Proof. intros a b c H1 H2. unfold Rmin. case (Rle_dec a b); intro H. apply H1. apply H2. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions