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