proposition: Theorem P_Rmin : forall (P : R -> Prop) (x y : R), P x -> P y -> P (Rmin x y).
proof: Proof. intros P x y H1 H2; unfold Rmin in |- *; case (Rle_dec x y); auto. Qed.
imports: Coq(ZArith Classical_Prop) Coq(Rbase Rfunctions Ranalysis Rtrigo)