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