(* This file was originally generated by why.
   It can be modified; only the generated parts will be overwritten. *)

Require Export max_spec_why.

(* Why obligation from file "", line 0, characters 0-0: *)
(*Why goal*) Lemma max_impl_po_1 : 
  forall (x: Z),
  forall (y: Z),
  forall (HW_1: x >= y),
  forall (res: Z),
  forall (HW_2: res = x),
  (res >= x /\ res >= y) /\ (forall (z:Z), (z >= x /\ z >= y -> z >= res)).
Proof.
intuition.
(* FILL PROOF HERE *)
Save.

(* Why obligation from file "", line 0, characters 0-0: *)
(*Why goal*) Lemma max_impl_po_2 : 
  forall (x: Z),
  forall (y: Z),
  forall (HW_3: x < y),
  forall (res: Z),
  forall (HW_4: res = y),
  (res >= x /\ res >= y) /\ (forall (z:Z), (z >= x /\ z >= y -> z >= res)).
Proof.
intuition.
(* FILL PROOF HERE *)
Save.

