proposition: Lemma max_assoc : forall a b c, max a (max b c) = max (max a b) c.
proof: Proof. intros. case (le_dec b c); intro H. rewrite (max_r H). case (le_dec a b); intro H'. rewrite (max_r (Nat.le_trans H' H)), (max_r H'), (max_r H). refl. case (le_dec a c); intro H''; rewrite (max_l H'); refl. rewrite (max_l H). case (le_dec a b); intro H'. rewrite (max_r H'). apply (sym_equal (max_l H)). assert (H'' : c <= max a b). eapply Nat.le_trans. apply H. apply Nat.le_max_r. apply (sym_equal (max_l H'')). Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)