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