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