proposition: Lemma Rmax_assoc : forall a b c, Rmax a (Rmax b c) = Rmax (Rmax a b) c.
proof: Proof. intros a b c. unfold Rmax; destruct (Rle_dec b c); destruct (Rle_dec a b); destruct (Rle_dec a c); destruct (Rle_dec b c); auto with real; match goal with | id : ~ ?x <= ?y, id2 : ?x <= ?z |- _ => case id; apply Rle_trans with z; auto with real | id : ~ ?x <= ?y, id2 : ~ ?z <= ?x |- _ => case id; apply Rle_trans with z; auto with real end. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp