Section FromDichotomy.

Variable Array : Type -> Z -> Type.
Variable Array_read : forall A n, Array A n -> Z -> maybe A.
Hypothesis Array_read_ok : forall A n m (a : Array A n),
  m < n -> is_defined _ (Array_read _ _ a m) = true.

Variable Array_read_default : forall A, A -> forall n, Array A n -> Z -> A.
Hypothesis Array_read_default_correct : forall A d n m (a : Array A n),
  m < n -> Array_read _ _ a m = defined _ (Array_read_default _ d _ a m).

Lemma reduce_div_le : forall a b c,
  0 < c ->
  a * c <= b ->
  a <= b / c.
Proof.
  intros a b c Pc I.
  rewrite <- (Z_div_mult_full a c).
   apply Z_div_le; auto with zarith.
   auto with zarith.
Qed.
Hint Resolve reduce_div_le.


(* Here is a goal generated by Why3 (and changed a little for simplicity). *)

Theorem WP_parameter_dichotomic_sort : forall (a:Z) (n:Z), ((0%Z <
  a)%Z /\ ((0%Z <= n)%Z /\ (n = a))) -> ((0%Z <= (a - 1%Z)%Z)%Z ->
  forall (a1:(Array Z a)), (forall (i:Z), ((0%Z <= i)%Z /\ (i <= (a -
  1%Z)%Z)%Z) -> (((0%Z < a)%Z /\ ((0%Z <= i)%Z /\ (i < a)%Z)) /\
  ((((0%Z <= 0%Z)%Z /\ (0%Z < a)%Z) /\ ((0%Z <= i)%Z /\ (i < a)%Z))
  /\ forall (right1:Z) (left1:Z), (((0%Z <= left1)%Z /\ (left1 <
  a)%Z) /\ ((0%Z <= right1)%Z /\ (right1 < a)%Z)) -> (((left1 <
  right1)%Z -> (((0%Z <= (Zdiv (left1 + right1)%Z 2%Z))%Z /\ ((Zdiv
  (left1 + right1)%Z 2%Z) < a)%Z) /\ ((((Array_read_default _ 0 _ a1
  i) < (Array_read_default _ 0 _ a1 (Zdiv (left1 + right1)%Z 2%Z)))%Z
  -> forall (right2:Z), (right2 = (Zdiv (left1 + right1)%Z 2%Z)) ->
  ((((0%Z <= left1)%Z /\ (left1 < a)%Z) /\ ((0%Z <= right2)%Z /\
  (right2 < a)%Z)) /\ ((0%Z <= (right1 - left1)%Z)%Z /\ ((right2 -
  left1)%Z < (right1 - left1)%Z)%Z))) /\ ((~ ((Array_read_default _ 0
  _ a1 i) < (Array_read_default _ 0 _ a1 (Zdiv (left1 + right1)%Z
  2%Z)))%Z) -> forall (left2:Z), (left2 = ((Zdiv (left1 + right1)%Z
  2%Z) + 1%Z)%Z) -> ((((0%Z <= left2)%Z /\ (left2 < a)%Z) /\ ((0%Z <=
  right1)%Z /\ (right1 < a)%Z)) /\ ((0%Z <= (right1 - left1)%Z)%Z /\
  ((right1 - left2)%Z < (right1 - left1)%Z)%Z)))))) /\ ((~ (left1 <
  right1)%Z) -> ((left1 = right1) /\ ((0%Z <= (i - left1)%Z)%Z ->
  forall (j:Z), ((0%Z <= j)%Z /\ (j <= (i - left1)%Z)%Z) -> ((0%Z <
  a)%Z /\ (((0%Z <= (i - j)%Z)%Z /\ ((i - j)%Z < a)%Z) /\ ((0%Z <=
  ((i - j)%Z + 1%Z)%Z)%Z /\ (((i - j)%Z + 1%Z)%Z < a)%Z)))))))))) /\
  (0%Z < a)%Z).
Proof.
    repeat split; auto with zarith.
    (* ... *)
Qed.

End FromDichotomy.