proposition: Theorem max2_correct : forall n m:nat, m <= max n m.
proof: Proof. intros n m; unfold max; case (le_gt_dec n m); auto with arith. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure chap9