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