proposition: Lemma max_or : forall a b, (max a b = a) \/ (max a b = b).
proof: Proof. induction a; simpl; sp; try omega. destruct b; auto. assert (max a b = a \/ max a b = b) by apply IHa; sp. Qed.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega