proposition: Theorem max_assoc : ∀ m n p, max m (max n p) = max (max m n) p.
proof: Proof. intros m n p. destruct n as [n| ]; [ simpl | destruct m; reflexivity ]. destruct m as [m| ]; [ simpl | reflexivity ]. destruct p as [p| ]; [ simpl | reflexivity ]. rewrite Nat.max_assoc; reflexivity. Qed.
imports: Utf8 Compare_dec NPeano Misc