proposition: Lemma Rmin_le_le_le : forall x y z, z <= Rmin x y <-> z <= x /\ z <= y.
proof: Proof. intros x y z ; unfold Rmin ; destruct (Rle_dec x y) ; split ; intuition. transitivity x ; assumption. transitivity y ; [| left ; apply Rnot_le_lt] ; assumption. Qed.
imports: RIneq MyNeq Rfunctions Lra