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