proposition: Lemma Rmax_assoc : forall x y z, Rmax x (Rmax y z) = Rmax (Rmax x y) z.
proof: Proof. intros x y z. unfold Rmax. destruct (Rle_dec x y) as [Hxy|Hxy]. destruct (Rle_dec y) as [Hyz|Hyz]. assert (Hxz := Rle_trans _ _ _ Hxy Hyz). now case Rle_dec. now case Rle_dec. destruct (Rle_dec y) as [Hyz|Hyz]. easy. case Rle_dec ; try easy. intros _. case Rle_dec ; try easy. intros Hxz. elim Hxy. apply Rle_trans with (1 := Hxz). apply Rlt_le. now apply Rnot_le_lt. Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)