proposition: Lemma Rmin_lt_lt_lt : 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. apply Rlt_le_trans with x ; assumption. transitivity y ; [| apply Rnot_le_lt] ; assumption. Qed.
imports: RIneq MyNeq Rfunctions Lra