Library abstraction_phd_aux



Set Implicit Arguments.

Require Import Setoid.
Require Import floor.
Require Import Bool.
Require Import Omega.
Require Import ZArith.
Require Import Znumtheory.
Require Import Z_misc.
Require Import QArith.
Require Import Q_misc.
Require Import comparison.
Require Import misc.
Require Import ibw_def.
Require Import ibw_aux.
Require Import ibw_prop.
Require Import abstraction_phd_def.

Section Abstraction_phd_def.

  Definition abs_equal (a1: abstraction_phd) (a2:abstraction_phd) :=
    (abs_r a1 == abs_r a2) /\
    (abs_b1 a1) == (abs_b1 a2) /\
    (abs_b0 a1) == (abs_b0 a2).

  Instance abs_equal_is_equiv : Equivalence abs_equal.
  Proof.
    constructor ; unfold abs_equal ; red ; intuition.
    transitivity (abs_r y) ; auto.
    transitivity (abs_b1 y) ; auto.
    transitivity (abs_b0 y) ; auto.
  Qed.

End Abstraction_phd_def.

Definition abs_equiv (a1: abstraction_phd) (a2:abstraction_phd) :=
  abs_included a1 a2 /\ abs_included a2 a1.

Definition abs_equiv_test (a1: abstraction_phd) (a2:abstraction_phd) :=
  abs_included_test a1 a2 /\ abs_included_test a2 a1.

Section abstraction_equivalence_properties.

  Property abs_included_test_impl_abs_included:
    forall a1 a2: abstraction_phd,
    forall H_a1_in_test_a2: abs_included_test a1 a2,
    abs_included a1 a2.
  Proof.
    intros.
    unfold abs_included.
    intros.
    unfold in_abstraction_phd.
    intros.
    case_eq i.
      intros H_i.
      rewrite H_i in H_i_ge_1.
      absurd ((0 >= 1)%nat); auto.
      apply gt_not_le.
      auto.

      intros i' H_i.
      rewrite <- H_i.
      elim (H_w_in_a1 i H_i_ge_1).
      intros H_le H_ge.
      elim H_a1_in_test_a2.
      intros H_r H_tmp.
      elim H_tmp; clear H_tmp.
      intros H_one H_zero.
      rewrite <- H_r.
      split.
        intro H_w.
        apply
          (Qle_trans
            (ones w i)
            (abs_r a1 * i + abs_b1 a1)
            (abs_r a1 * i + abs_b1 a2)); auto.
        apply Qplus_le_compat; auto.
        apply Qle_refl.

        intro H_w.
        apply
          (Qle_trans
            (abs_r a1 * i + abs_b0 a2)
            (abs_r a1 * i + abs_b0 a1)
            (ones w i)); auto.
        apply Qplus_le_compat; auto.
        apply Qle_refl.
  Qed.

  Property w_in_a1_and_a1_in_a2_impl_w_in_a2:
    forall w a1 a2,
    forall H_wf_a1: well_formed_abstraction_phd a1,
    forall H_wf_a2: well_formed_abstraction_phd a2,
    forall H_a1_in_a2: abs_included_test a1 a2,
    forall H_w_in_a1: in_abstraction_phd w a1,
    in_abstraction_phd w a2.
  Proof.
    intros.
    unfold in_abstraction_phd.
    intros i H_i_ge_1.
    split.
      intro H_w.
      unfold in_abstraction_phd in H_w_in_a1.
      generalize (H_w_in_a1 i H_i_ge_1).
      intro H_w_in_a1_i.
      elim H_w_in_a1_i.
      intros H_w_in_a1_true H_w_in_a1_false.
      generalize (H_w_in_a1_true H_w).
      clear H_w_in_a1_i H_w_in_a1_true H_w_in_a1_false.
      intro H_w_le_a1.
      elim H_a1_in_a2.
      intros H_r1_eq_r2 H_aux.
      elim H_aux. clear H_aux.
      intros H_d2_le_d1 H_D1_le_D2.
      rewrite <- H_r1_eq_r2.
      apply (Qle_trans
        (ones w i)
        (abs_r a1 * i + abs_b1 a1)
        (abs_r a1 * i + abs_b1 a2)
        H_w_le_a1).
      apply Qplus_le_compat; auto.
      apply Qmult_le_compat_r; try solve [apply Qle_refl].
      unfold Q_of_nat, Qle; simpl; auto with zarith.

      intro H_w.
      unfold in_abstraction_phd in H_w_in_a1.
      generalize (H_w_in_a1 i H_i_ge_1).
      intro H_w_in_a1_i.
      elim H_w_in_a1_i.
      intros H_w_in_a1_true H_w_in_a1_false.
      generalize (H_w_in_a1_false H_w).
      clear H_w_in_a1_i H_w_in_a1_true H_w_in_a1_false.
      intro H_a1_le_w.
      elim H_a1_in_a2.
      intros H_r1_eq_r2 H_aux.
      elim H_aux. clear H_aux.
      intros H_d2_le_d1 H_D1_le_D2.
      rewrite <- H_r1_eq_r2.
      apply
        (Qle_trans
          (abs_r a1 * i + abs_b0 a2)
          (abs_r a1 * i + abs_b0 a1)
          (ones w i));
        auto.
      apply Qplus_le_compat; auto.
      apply Qmult_le_compat_r; try solve [apply Qle_refl].
      apply (Qle_trans 0 1 i).
        unfold Q_of_nat, Qle; simpl; auto with zarith.
        apply (le_impl_Qle H_i_ge_1).
  Qed.

  Property abs_weakening_aux:
    forall a1 a2: abstraction_phd,
    forall H_one: abs_b1 a1 <= abs_b1 a2,
    forall H_abs_b0: abs_b0 a1 >= abs_b0 a2,
    forall H_r: abs_r a1 == abs_r a2,
    abs_included_test a1 a2.
  Proof.
    intros.
    unfold abs_included_test.
    repeat split; auto.
  Qed.

  Property abs_weakening_0:
    forall a1 a2: abstraction_phd,
    forall H_abs_b01: abs_b0 a1 > 0,
    forall H_r: abs_r a1 == abs_r a2,
    forall H_one: abs_b1 a1 == abs_b1 a2,
    forall H_abs_b02: abs_b0 a2 == 0,
    abs_included_test a1 a2.
  Proof.
    intros.
    eapply abs_weakening_aux; auto.
    rewrite H_one.
    apply Qle_refl.
    rewrite H_abs_b02.
    eapply Qlt_le_weak.
    assumption.
  Qed.

  Property abs_equal_sym:
    forall a1 a2: abstraction_phd,
    forall H_a1_eq_a2: abs_equal a1 a2,
    abs_equal a2 a1.
  Proof.
    intros.
    elim H_a1_eq_a2.
    intros H_r H_tmp.
    elim H_tmp; clear H_tmp.
    intros H_one H_zero.
    repeat split;
      symmetry;
      assumption.
  Qed.

  Property abs_equal_impl_abs_included_test:
    forall a1 a2: abstraction_phd,
    forall H_a1_eq_a2: abs_equal a1 a2,
    abs_included_test a1 a2.
  Proof.
    intros.
    elim H_a1_eq_a2.
    intros H_r H_tmp.
    elim H_tmp; clear H_tmp.
    intros H_one H_zero.
    repeat split.
      trivial.
      rewrite H_one.
      apply Qle_refl.
      rewrite H_zero.
      apply Qle_refl.
  Qed.

  Property abs_equal_impl_abs_equiv_test:
    forall a1 a2: abstraction_phd,
    forall H_a1_eq_a2: abs_equal a1 a2,
    abs_equiv_test a1 a2.
  Proof.
    intros.
    split.
      apply abs_equal_impl_abs_included_test; auto.
      apply abs_equal_impl_abs_included_test; auto.
      apply abs_equal_sym.
      assumption.
  Qed.

  Property abs_equiv_test_impl_abs_equal:
    forall a1 a2: abstraction_phd,
    forall H_a1_eq_a2: abs_equiv_test a1 a2,
    abs_equal a1 a2.
  Proof.
    intros.
    elim H_a1_eq_a2.
    intros H_tmp1 H_tmp2.
    elim H_tmp1; clear H_tmp1.
    intros H_r H_tmp'.
    elim H_tmp'; clear H_tmp'.
    intros H_abs_b11_le_abs_b12 H_abs_b02_le_abs_b01.
    elim H_tmp2; clear H_tmp2.
    intros H_r' H_tmp'.
    elim H_tmp'; clear H_tmp' H_r'.
    intros H_abs_b12_le_abs_b11 H_abs_b01_le_abs_b02.
    repeat split.
      trivial.
      apply Qle_antisym; assumption.
      apply Qle_antisym; assumption.
  Qed.

  Property abs_equal_correctness:
    forall a1 a2: abstraction_phd,
    forall H_wf1: well_formed_abstraction_phd a1,
    forall H_wf2: well_formed_abstraction_phd a2,
    forall w: ibw,
    forall H_w_in_a1: in_abstraction_phd w a1,
    forall H_eq: abs_equal a1 a2,
    in_abstraction_phd w a2.
  Proof.
    intros.
    apply abs_equal_impl_abs_included_test in H_eq.
    exact (w_in_a1_and_a1_in_a2_impl_w_in_a2 H_wf1 H_wf2 H_eq H_w_in_a1).
  Qed.

  Property well_formed_abstraction_phd_abs_equal_compat:
    forall a1 a2: abstraction_phd,
    forall H_eq: abs_equal a1 a2,
    forall H_wf1: well_formed_abstraction_phd a1,
      well_formed_abstraction_phd a2.
  Proof.
    intros.
    destruct H_eq as [H_r [H_b1 H_b0]].
    unfold well_formed_abstraction_phd in *.
    rewrite <- H_r.
    assumption.
  Qed.

End abstraction_equivalence_properties.

Fixpoint ones_early_opt (a:abstraction_phd) (i:nat) { struct i } :=
  match i with
  | O => Some O
  | S i' =>
    let ones_i'_opt := ones_early_opt a i' in
    match ones_i'_opt with
    | None => None
    | Some ones_i' =>
      match Qcompare (S ones_i') (abs_r a * i + abs_b1 a) with
      | Lt | Eq => Some (S ones_i')
      | Gt =>
        match Qcompare (abs_r a * i + abs_b0 a) ones_i' with
        | Lt | Eq => Some (ones_i')
        | _ => None
        end
      end
    end
  end.

Fixpoint ones_late_opt (a:abstraction_phd) (i:nat) { struct i } :=
  match i with
  | O => Some O
  | S i' =>
    let ones_i'_opt := ones_late_opt a i' in
    match ones_i'_opt with
    | None => None
    | Some ones_i' =>
      match Qcompare (abs_r a * i + abs_b0 a) ones_i' with
      | Lt | Eq => Some (ones_i')
      | Gt =>
        match Qcompare (S ones_i') (abs_r a * i + abs_b1 a) with
        | Lt | Eq => Some (S ones_i')
        | Gt => None
        end
      end
    end
  end.

Definition non_empty_alt (a: abstraction_phd) :=
  forall i, (ones_late a i <= ones_early a i)%nat.

Section early_and_late_properties.

  Lemma red_ones_early:
    forall a i',
    (ones_early a (S i') =
     match S (ones_early a i') ?= abs_r a * S i' + abs_b1 a with
     | Eq => S (ones_early a i')
     | Lt => S (ones_early a i')
     | Gt => ones_early a i'
     end)%nat.
  Proof.
    intros.
    simpl.
    reflexivity.
  Qed.

  Lemma red_ones_late:
    forall a i',
    (ones_late a (S i') =
     match abs_r a * (S i') + abs_b0 a ?= ones_late a i' with
     | Lt | Eq => ones_late a i'
     | Gt => S (ones_late a i')
     end)%nat.
  Proof.
    intros.
    simpl.
    reflexivity.
  Qed.

  Lemma red_ones_early_opt:
    forall a i',
    (ones_early_opt a (S i') =
     match ones_early_opt a i' with
     | None => None
     | Some ones_i' =>
       match Qcompare (S ones_i') (abs_r a * S i' + abs_b1 a) with
       | Lt | Eq => Some (S ones_i')
       | Gt =>
         match Qcompare (abs_r a * S i' + abs_b0 a) ones_i' with
         | Lt | Eq => Some (ones_i')
         | _ => None
         end
       end
     end)%nat.
  Proof.
    intros.
    simpl.
    reflexivity.
  Qed.

  Lemma red_ones_late_opt:
    forall a i',
    (ones_late_opt a (S i') =
     match ones_late_opt a i' with
     | None => None
     | Some ones_i' =>
       match Qcompare (abs_r a * S i' + abs_b0 a) ones_i' with
       | Lt | Eq => Some (ones_i')
       | Gt =>
         match Qcompare (S ones_i') (abs_r a * S i' + abs_b1 a) with
         | Lt | Eq => Some (S ones_i')
         | Gt => None
         end
       end
     end)%nat.
  Proof.
    intros.
    simpl.
    reflexivity.
  Qed.

  Lemma ones_early_alt_remove_Zabs_nat:
    forall a:abstraction_phd,
    forall i,
    ((Z_of_nat (ones_early_alt a i))%Z =
      Zmax O (Zmin i (fl (abs_r a * i + abs_b1 a))))%Z.
  Proof.
    intros.
    unfold ones_early_alt.
    rewrite inj_Zabs_nat.
    elim (Zabs_spec (Zmax O (Zmin i (fl (abs_r a * i + abs_b1 a))))).
      intro H_tmp; destruct H_tmp.
      rewrite H0.
      reflexivity.
      intro H_tmp; destruct H_tmp.
      elim (Zmax_spec O (Zmin i (fl (abs_r a * i + abs_b1 a)))).
        intro H_tmp; destruct H_tmp.
        rewrite H2.
        auto.

        intro H_tmp; destruct H_tmp.
        rewrite H2 in H.
        assert (H_aux: Z_of_nat 0%nat = 0%Z); omega.
  Qed.

  Lemma ones_late_alt_remove_Zabs_nat:
    forall a:abstraction_phd,
    forall i,
    ((Z_of_nat (ones_late_alt a i))%Z =
      Zmax O (Zmin i (cg (abs_r a * i + abs_b0 a))))%Z.
  Proof.
    intros.
    unfold ones_late_alt.
    rewrite inj_Zabs_nat.
    elim (Zabs_spec (Zmax O (Zmin i (cg (abs_r a * i + abs_b0 a))))).
      intro H_tmp; destruct H_tmp.
      rewrite H0.
      reflexivity.
      intro H_tmp; destruct H_tmp.
      elim (Zmax_spec O (Zmin i (cg (abs_r a * i + abs_b0 a)))).
        intro H_tmp; destruct H_tmp.
        rewrite H2.
        auto.

        intro H_tmp; destruct H_tmp.
        rewrite H2 in H.
        assert (H_aux: Z_of_nat 0%nat = 0%Z); omega.
  Qed.

  Property ones_early_well_formed:
    forall a: abstraction_phd,
    well_formed_ones (ones_early a).
  Proof.
    intros.
    split.
      simpl.
      reflexivity.

      intro.
      simpl.
      case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
        intro H_cmp.
        left.
        reflexivity.

        intro H_cmp.
        left.
        reflexivity.

        intro H_cmp.
        right.
        reflexivity.
  Qed.

  Property ones_late_well_formed:
    forall a: abstraction_phd,
    well_formed_ones (ones_late a).
  Proof.
    intros.
    split.
      simpl.
      reflexivity.

      intro.
      simpl.
      case_eq (abs_r a * S i + abs_b0 a ?= ones_late a i);
      omega.
  Qed.

  Property w_early_well_formed:
    forall a,
    well_formed_ibw (w_early a).
  Proof.
    intros.
    unfold well_formed_ibw.
    simpl.
    reflexivity.
  Qed.

  Property w_late_well_formed:
    forall a,
    well_formed_ibw (w_late a).
  Proof.
    intros.
    unfold well_formed_ibw.
    simpl.
    reflexivity.
  Qed.

  Property ones_early_eq_ones_w_early:
    forall a: abstraction_phd,
    forall i,
    (ones_early a i = ones (w_early a) i)%nat.
  Proof.
    intros.
    case i.
      simpl.
      reflexivity.

      clear i.
      intro i'.
      induction i'.
        simpl.
        case_eq (1%nat ?= abs_r a * 1%nat + abs_b1 a);
          intros;
          simpl;
          reflexivity.

        assert (H_aux:
          (ones_early a (S (S i'))
           =
           match S (ones_early a (S i')) ?= abs_r a * (S (S i')) + abs_b1 a with
           | Eq => S (ones_early a (S i'))
           | Lt => S (ones_early a (S i'))
           | Gt => ones_early a (S i')
           end)%nat).
          simpl.
          reflexivity.
        rewrite H_aux; clear H_aux.
        assert (H_aux:
          (ones (w_early a) (S (S i'))
           =
           ((if negb
             (beq_nat
               match S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a with
               | Eq => S (ones_early a (S i'))
               | Lt => S (ones_early a (S i'))
               | Gt => ones_early a (S i')
               end (ones_early a (S i')))
             then 1
             else 0) + ones (w_early a) (S i'))%nat)%nat).
          simpl.
          reflexivity.
        rewrite H_aux; clear H_aux.
        case_eq (S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a).
          intro.
          assert (H_aux:
            beq_nat (S (ones_early a (S i'))) (ones_early a (S i')) = false).
            apply S_n_nbeq_n.
          rewrite H_aux; clear H_aux.
          assert (H_aux: ((if negb false then 1 else 0) = 1)%nat).
            auto.
          rewrite H_aux; clear H_aux.
          unfold plus.
          rewrite IHi'.
          reflexivity.

          intro.
          assert (H_aux:
            beq_nat (S (ones_early a (S i'))) (ones_early a (S i')) = false).
            apply S_n_nbeq_n.
          rewrite H_aux; clear H_aux.
          assert (H_aux: ((if negb false then 1 else 0) = 1)%nat).
            auto.
          rewrite H_aux; clear H_aux.
          unfold plus.
          rewrite IHi'.
          reflexivity.

          intro.
          assert (H_aux:
            beq_nat ((ones_early a (S i'))) (ones_early a (S i')) = true).
            rewrite <- beq_nat_refl.
            trivial.
          rewrite H_aux; clear H_aux.
          assert (H_aux: ((if negb true then 1 else 0) = 0)%nat).
            auto.
          rewrite H_aux; clear H_aux.
          unfold plus.
          rewrite IHi'.
          reflexivity.
  Qed.

  Property ones_late_eq_ones_w_late:
    forall a: abstraction_phd,
    forall i,
    (ones_late a i = ones (w_late a) i)%nat.
  Proof.
    intros.
    case i.
      simpl.
      reflexivity.

      clear i.
      intro i'.
      induction i'.
        simpl.
        case_eq (abs_r a * 1%nat + abs_b0 a ?= 0%nat);
          intros;
          simpl;
          reflexivity.

        rewrite red_ones_late.
        assert (H_aux:
          (ones (w_late a) (S (S i'))
           =
           ((if negb
             (beq_nat
               match abs_r a * S (S i') + abs_b0 a ?= ones_late a (S i') with
               | Eq | Lt => ones_late a (S i')
               | Gt => S (ones_late a (S i'))
               end (ones_late a (S i')))
             then 1
             else 0) + ones (w_late a) (S i'))%nat)%nat).
          simpl.
          reflexivity.
        rewrite H_aux; clear H_aux.

        case_eq (abs_r a * S (S i') + abs_b0 a ?= ones_late a (S i')).
          intro.
          assert (H_aux:
            beq_nat ((ones_late a (S i'))) (ones_late a (S i')) = true).
            rewrite <- beq_nat_refl.
            trivial.
          rewrite H_aux; clear H_aux.
          assert (H_aux: ((if negb true then 1 else 0) = 0)%nat).
            auto.
          rewrite H_aux; clear H_aux.
          unfold plus.
          rewrite IHi'.
          reflexivity.

          intro.
          assert (H_aux:
            beq_nat ((ones_late a (S i'))) (ones_late a (S i')) = true).
            rewrite <- beq_nat_refl.
            trivial.
          rewrite H_aux; clear H_aux.
          assert (H_aux: ((if negb true then 1 else 0) = 0)%nat).
            auto.
          rewrite H_aux; clear H_aux.
          unfold plus.
          rewrite IHi'.
          reflexivity.

          intro.
          assert (H_aux:
            beq_nat (S (ones_late a (S i'))) (ones_late a (S i')) = false).
            apply S_n_nbeq_n.
          rewrite H_aux; clear H_aux.
          assert (H_aux: ((if negb false then 1 else 0) = 1)%nat).
            auto.
          rewrite H_aux; clear H_aux.
          unfold plus.
          rewrite IHi'.
          reflexivity.
  Qed.

  Property ones_early_eq_ones_early_alt:
    forall a: abstraction_phd,
    forall H_wf: well_formed_abstraction_phd a,
    forall i,
    ones_early a i = ones_early_alt a i.
  Proof.
   induction i.
     simpl.
     apply Zeq_impl_nat_eq.
     rewrite ones_early_alt_remove_Zabs_nat.
     elim (Zmax_spec O (Zmin O%nat (fl (abs_r a * O%nat + abs_b1 a)))).
       intro H_tmp; destruct H_tmp.
       rewrite H0.
       reflexivity.

       intro H_tmp; destruct H_tmp.
       rewrite H0.
       elim (Zmin_spec 0%nat (fl (abs_r a * 0%nat + abs_b1 a))).
         intro H_tmp; destruct H_tmp.
         rewrite H2.
         reflexivity.
         intro H_tmp; destruct H_tmp.
         rewrite H2 in H.
         congruence.

     apply Zeq_impl_nat_eq.
     rewrite ones_early_alt_remove_Zabs_nat.
     elim (Zmax_spec O (Zmin (S i) (fl (abs_r a * S i + abs_b1 a)))).
       intro H_tmp; destruct H_tmp.
       elim (Zmin_spec (S i) (fl (abs_r a * (S i) + abs_b1 a))).
         intro H_tmp; destruct H_tmp.
         rewrite H0 in *.
         rewrite H2 in *.
         absurd (0%nat >= S i)%Z; auto.

         intro H_tmp; destruct H_tmp.
         rewrite H0 in *.
         rewrite H2 in *.

         assert (H_cc_aux1: ones_early a i = 0%nat).
           rewrite IHi.
           apply Zeq_impl_nat_eq.
           rewrite ones_early_alt_remove_Zabs_nat.
           rewrite Zmax_left; auto.
           rewrite Zmin_right.
             apply
               (Zge_trans
                 0%nat
                 (fl (abs_r a * S i + abs_b1 a))
                 (fl (abs_r a * i + abs_b1 a))); auto.
             apply Zle_ge.
             apply fl_monotone_linear.
             assert (H_aux:
               abs_r a * i + abs_b1 a ==
               abs_r a * i + abs_b1 a + 0).
               ring.
             rewrite H_aux; clear H_aux.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               abs_r a * (i + 1) + abs_b1 a ==
               abs_r a * i + abs_b1 a + abs_r a).
               ring.
             rewrite H_aux; clear H_aux.
             apply Qplus_le_compat; try solve [ apply Qle_refl ].
             destruct H_wf; assumption.

             apply Zgt_impl_Zge.
             assert (H_aux: (i + 1%nat)%Z = S i).
               assert (H_aux: (Z_of_nat (i + 1%nat)%nat = (i + 1%nat)%Z)%Z).
                 apply inj_plus.
               rewrite <- H_aux; clear H_aux.
               rewrite plus_comm.
               simpl.
               reflexivity.
             rewrite H_aux; clear H_aux.
             apply (Zgt_le_trans
               (S i)
               (fl (abs_r a * S i + abs_b1 a))
               (fl (abs_r a * i + abs_b1 a))); auto.
             apply fl_monotone_linear.
             assert (H_aux:
               abs_r a * i + abs_b1 a ==
               abs_r a * i + abs_b1 a + 0).
               ring.
             rewrite H_aux; clear H_aux.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               abs_r a * (i + 1) + abs_b1 a ==
               abs_r a * i + abs_b1 a + abs_r a).
               ring.
             rewrite H_aux; clear H_aux.
             apply Qplus_le_compat; try solve [ apply Qle_refl ].
             destruct H_wf; assumption.
         assert (H_cc_aux2: S (ones_early a i) > abs_r a * S i + abs_b1 a).
           clear H0; clear H2.
           rewrite H_cc_aux1.
           apply (Qlt_le_trans
             (abs_r a * S i + abs_b1 a)
             (fl (abs_r a * S i + abs_b1 a) + 1)
             1).
           destruct (fl_def (abs_r a * S i + abs_b1 a)); assumption.
           assert (H_aux: forall x, fl x + 1 == (fl x + 1)%Z).
             intro; unfold Qeq, Qplus, Q_of_nat; simpl; ring_simplify; auto.
           rewrite H_aux; clear H_aux.
           apply Zle_impl_Qle.
           assert (H_aux: (1 = 0 + 1)%Z).
             auto with zarith.
           rewrite H_aux; clear H_aux.
           apply Zplus_le_compat_r.
           apply Zge_le.
           assumption.

         rewrite red_ones_early.
         case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a);
           try solve [ intro H_cmp; apply inj_eq; assumption].
           intro H_cmp.
           rewrite <- Qeq_alt in H_cmp.
           absurd (S (ones_early a i) > abs_r a * S i + abs_b1 a); auto.
           apply Qle_not_lt.
           rewrite H_cmp.
           apply Qle_refl.

           intro H_cmp.
           rewrite <- Qlt_alt in H_cmp.
           absurd (S (ones_early a i) < abs_r a * S i + abs_b1 a); auto.
           apply Qle_not_lt.
           apply Qlt_le_weak.
           assumption.

       intro H_tmp; destruct H_tmp.
       elim (Zmin_spec (S i) (fl (abs_r a * (S i) + abs_b1 a))).
         intro H_tmp; destruct H_tmp.
         rewrite H0 in *.
         rewrite H2 in *.
         assert (H_cc_aux1: ones_early a i = i).
           rewrite IHi.
           apply Zeq_impl_nat_eq.
           rewrite ones_early_alt_remove_Zabs_nat.
           rewrite Zmin_left.
           rewrite Zmax_right.
           trivial.
           apply inj_le.
           auto with arith.
           apply Zlt_impl_Zle.
           apply (Zlt_le_trans
             i
             (S i)
             (fl (abs_r a * i + abs_b1 a) + 1%nat)).
             apply inj_lt.
             auto with arith.
             rewrite <- fl_plus_int_rewrite.
             apply (Zle_trans
               (S i)
               (fl (abs_r a * S i + abs_b1 a))
               (fl (abs_r a * i + abs_b1 a + 1))); auto.
             apply fl_monotone_linear.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               abs_r a * (i + 1) + abs_b1 a ==
               abs_r a * i + abs_b1 a + abs_r a).
               ring.
             rewrite H_aux; clear H_aux.
             apply Qplus_le_compat; try solve [ apply Qle_refl ].
             destruct H_wf; assumption.

         assert (H_cc_aux2: S (ones_early a i) <= abs_r a * S i + abs_b1 a).
           rewrite H_cc_aux1.
           apply (Qle_trans
             (S i)
             (fl (abs_r a * S i + abs_b1 a))
             (abs_r a * S i + abs_b1 a));
             try solve [ elim (fl_def (abs_r a * S i + abs_b1 a)); auto ].
           apply Zle_impl_Qle.
           assumption.
         rewrite red_ones_early.
         case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a); auto.
         intro H_cmp.
         rewrite Qle_alt in H_cc_aux2.
         rewrite H_cmp in H_cc_aux2.
         congruence.

         intro H_tmp; destruct H_tmp.
         rewrite H0 in *.
         rewrite H2 in *.
         clear H2 H0.
         rewrite ones_early_eq_ones_w_early.
         case_eq (w_early a (S i)).
           intro H_w_early.
           rewrite ones_S_i_eq_S_ones_i; auto.
           rewrite <- ones_early_eq_ones_w_early.
           rewrite IHi.
           assert (H_aux: (Z_of_nat (1 + ones_early_alt a i)) = (1 + ones_early_alt a i)%Z).
             apply inj_plus.
           rewrite H_aux; clear H_aux.
           assert (H_cmp: S (ones_early a i) <= abs_r a * S i + abs_b1 a).
             rewrite Qle_alt.
             case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a);
               try solve [congruence].
               intro H_cmp;
               simpl in H_w_early;
               rewrite H_cmp in H_w_early;
               rewrite <- beq_nat_refl in H_w_early;
               simpl in H_w_early;
               congruence.

           rewrite IHi in H_cmp.
           apply Zle_antisym.
             assert (TH_aux: forall (x: nat) (y: Z), (x < y)%Z -> (1%nat + x <= y)%Z).
               intros x y H_lt.
               replace (1%nat + x)%Z with (- ( -(1) + - x))%Z by ring.
               apply Zle_0_minus_le.
               unfold Zminus.
               rewrite Zopp_involutive.
               rewrite Zplus_assoc.
               apply Zlt_left.
               assumption.
             apply TH_aux; auto.

             apply Qlt_impl_Zlt.

             apply -> (Qlt_plus 1%nat).
             assert (H_aux: (1%nat + ones_early_alt a i) == S (ones_early_alt a i)).
               rewrite Qplus_comm.
               rewrite n_plus_1_eq_S_n.
               apply Qeq_refl.
             rewrite H_aux; clear H_aux.
             rewrite Qplus_comm.

             apply
               (Qle_lt_trans
                 (S (ones_early_alt a i))
                 (abs_r a * S i + abs_b1 a)
                 (fl (abs_r a * S i + abs_b1 a) + 1)); auto.
             elim (fl_def (abs_r a * S i + abs_b1 a)); auto.

             rewrite ones_early_alt_remove_Zabs_nat.
             rewrite Zmin_right; auto.
               rewrite Zmax_right.
                 rewrite Zplus_comm.
                 rewrite <- fl_plus_int_rewrite.
                 apply fl_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   abs_r a * (i + 1) + abs_b1 a ==
                   abs_r a * i + abs_b1 a + abs_r a).
                   ring.
                 rewrite H_aux; clear H_aux.
                 apply Qplus_le_compat; try solve [apply Qle_refl].
                 replace 1%Z with (Z_of_nat 1); auto.
                 destruct H_wf; auto.

                 apply Zlt_impl_Zle.
                 apply
                   (Zlt_le_trans
                     0%nat
                     (fl (abs_r a * S i + abs_b1 a))
                     (fl (abs_r a * i + abs_b1 a) + 1%nat)); auto.
                 rewrite <- fl_plus_int_rewrite.
                 apply fl_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   abs_r a * (i + 1) + abs_b1 a ==
                   abs_r a * i + abs_b1 a + abs_r a).
                   ring.
                 rewrite H_aux; clear H_aux.
                 apply Qplus_le_compat; try solve [apply Qle_refl].
                 destruct H_wf; auto.

               apply
                 (Zge_trans
                   i
                   (fl (abs_r a * S i + abs_b1 a))
                   (fl (abs_r a * i + abs_b1 a))).
                 assert (TH_aux: forall (x: nat) (y: Z), (S x > y)%Z -> (x >= y)%Z).
                   intros x y H_gt.
                   apply Zgt_impl_Zge.
                   assert (H_aux: (x + 1%nat)%Z = S x).
                     assert (H_aux: (Z_of_nat (x + 1%nat)%nat = (x + 1%nat)%Z)%Z).
                       apply inj_plus.
                     rewrite <- H_aux; clear H_aux.
                     rewrite plus_comm.
                     simpl.
                     reflexivity.
                   rewrite H_aux; clear H_aux.
                   assumption.
                 apply TH_aux; auto.
                 apply Zle_ge.
                 apply fl_monotone_linear.
                 apply Qplus_le_compat; try solve [ apply Qle_refl ].
                 rewrite Qmult_comm.
                 assert (H_aux: abs_r a * S i == S i * abs_r a).
                   ring.
                 rewrite H_aux; clear H_aux.
                 apply Qmult_le_compat_r; try solve [ apply le_impl_Qle; auto].
                 destruct H_wf; auto.

           intro H_w_early.
           rewrite ones_S_i_eq_ones_i; auto.
           rewrite <- ones_early_eq_ones_w_early.
           rewrite IHi.
           assert (H_cmp: S (ones_early a i) > abs_r a * S i + abs_b1 a).
             rewrite Qgt_alt.
             case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
               intro H_cmp.
               simpl in H_w_early.
               rewrite H_cmp in H_w_early.
               rewrite S_n_nbeq_n in H_w_early.
               simpl in H_w_early;
               congruence.
               intro H_cmp.
               simpl in H_w_early.
               rewrite H_cmp in H_w_early.
               rewrite S_n_nbeq_n in H_w_early.
               simpl in H_w_early;
               congruence.
               intro H_cmp.
               auto.
           rewrite IHi in H_cmp.
           apply Zle_antisym.
             rewrite ones_early_alt_remove_Zabs_nat.
             rewrite Zmin_right; auto.
               rewrite Zmax_right.
                 apply fl_monotone_linear.
                 assert (H_aux:
                   abs_r a * i + abs_b1 a ==
                   abs_r a * i + abs_b1 a + 0).
                   ring.
                 rewrite H_aux; clear H_aux.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   abs_r a * (i + 1) + abs_b1 a ==
                   abs_r a * i + abs_b1 a + abs_r a).
                   ring.
                 rewrite H_aux; clear H_aux.
                 apply Qplus_le_compat; try solve [apply Qle_refl].
                 destruct H_wf; assumption.

                 apply Zlt_impl_Zle.
                 apply (Zlt_le_trans
                   0%nat
                   (fl (abs_r a * S i + abs_b1 a))
                   (fl (abs_r a * i + abs_b1 a) + 1%nat)); auto.
                 rewrite <- fl_plus_int_rewrite.
                 apply fl_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   abs_r a * (i + 1) + abs_b1 a ==
                   abs_r a * i + abs_b1 a + abs_r a).
                   ring.
                 rewrite H_aux; clear H_aux.
                 apply Qplus_le_compat; try solve [apply Qle_refl].
                 destruct H_wf; auto.

               apply
                 (Zge_trans
                   i
                   (fl (abs_r a * S i + abs_b1 a))
                   (fl (abs_r a * i + abs_b1 a))).
                 assert (TH_aux: forall (x: nat) (y: Z), (S x > y)%Z -> (x >= y)%Z).
                   intros x y H_gt.
                   apply Zgt_impl_Zge.
                   assert (H_aux: (x + 1%nat)%Z = S x).
                     assert (H_aux: (Z_of_nat (x + 1%nat)%nat = (x + 1%nat)%Z)%Z).
                       apply inj_plus.
                     rewrite <- H_aux; clear H_aux.
                     rewrite plus_comm.
                     simpl.
                     reflexivity.
                   rewrite H_aux; clear H_aux.
                   assumption.
                 apply TH_aux.
                 auto.
                 apply Zle_ge.
                 apply fl_monotone_linear.
                 apply Qplus_le_compat; try solve [ apply Qle_refl ].
                 rewrite Qmult_comm.
                 assert (H_aux: abs_r a * S i == S i * abs_r a).
                   ring.
                 rewrite H_aux; clear H_aux.
                 apply Qmult_le_compat_r; try solve [ apply le_impl_Qle; auto].
                 destruct H_wf; auto.

             apply Zlt_impl_Zle.
             apply Qlt_impl_Zlt.
             apply
               (Qle_lt_trans
                 (fl (abs_r a * S i + abs_b1 a))
                 (abs_r a * S i + abs_b1 a)
                 (ones_early_alt a i + 1%nat)%Z); auto.
             elim (fl_def (abs_r a * S i + abs_b1 a)); auto.
             rewrite <- inj_plus.
             assert (H_aux: (ones_early_alt a i + 1%nat)%nat = S (ones_early_alt a i)).
               rewrite plus_comm.
               simpl.
               reflexivity.
             rewrite H_aux; clear H_aux.
             assumption.
  Qed.

  Property ones_late_eq_ones_late_alt:
    forall a: abstraction_phd,
    forall H_wf: well_formed_abstraction_phd a,
    forall i,
    ones_late a i = ones_late_alt a i.
  Proof.
   induction i.
     simpl.
     apply Zeq_impl_nat_eq.
     rewrite ones_late_alt_remove_Zabs_nat.
     elim (Zmax_spec O (Zmin O%nat (cg (abs_r a * O%nat + abs_b0 a)))).
       intro H_tmp; destruct H_tmp.
       rewrite H0.
       reflexivity.

       intro H_tmp; destruct H_tmp.
       rewrite H0.
       elim (Zmin_spec 0%nat (cg (abs_r a * 0%nat + abs_b0 a))).
         intro H_tmp; destruct H_tmp.
         rewrite H2.
         reflexivity.
         intro H_tmp; destruct H_tmp.
         rewrite H2 in H.
         congruence.

     apply Zeq_impl_nat_eq.
     rewrite ones_late_alt_remove_Zabs_nat.
     elim (Zmax_spec O (Zmin (S i) (cg (abs_r a * S i + abs_b0 a)))).
       intro H_tmp; destruct H_tmp.
       elim (Zmin_spec (S i) (cg (abs_r a * (S i) + abs_b0 a))).
         intro H_tmp; destruct H_tmp.
         rewrite H0 in *.
         rewrite H2 in *.
         absurd (0%nat >= S i)%Z; auto.

         intro H_tmp; destruct H_tmp.
         rewrite H0 in *.
         rewrite H2 in *.

         assert (H_cc_aux1: ones_late a i = 0%nat).
           rewrite IHi.
           apply Zeq_impl_nat_eq.
           rewrite ones_late_alt_remove_Zabs_nat.
           rewrite Zmax_left; auto.
           rewrite Zmin_right.
             apply
               (Zge_trans
                 0%nat
                 (cg (abs_r a * S i + abs_b0 a))
                 (cg (abs_r a * i + abs_b0 a))); auto.
             apply Zle_ge.
             apply cg_monotone_linear.
             assert (H_aux:
               abs_r a * i + abs_b0 a ==
               abs_r a * i + abs_b0 a + 0).
               ring.
             rewrite H_aux; clear H_aux.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               abs_r a * (i + 1) + abs_b0 a ==
               abs_r a * i + abs_b0 a + abs_r a).
               ring.
             rewrite H_aux; clear H_aux.
             apply Qplus_le_compat; try solve [ apply Qle_refl ].
             destruct H_wf; assumption.

             apply Zgt_impl_Zge.
             assert (H_aux: (i + 1%nat)%Z = S i).
               assert (H_aux: (Z_of_nat (i + 1%nat)%nat = (i + 1%nat)%Z)%Z).
                 apply inj_plus.
               rewrite <- H_aux; clear H_aux.
               rewrite plus_comm.
               simpl.
               reflexivity.
             rewrite H_aux; clear H_aux.
             apply (Zgt_le_trans
               (S i)
               (cg (abs_r a * S i + abs_b0 a))
               (cg (abs_r a * i + abs_b0 a))); auto.
             apply cg_monotone_linear.
             assert (H_aux:
               abs_r a * i + abs_b0 a ==
               abs_r a * i + abs_b0 a + 0).
               ring.
             rewrite H_aux; clear H_aux.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               abs_r a * (i + 1) + abs_b0 a ==
               abs_r a * i + abs_b0 a + abs_r a).
               ring.
             rewrite H_aux; clear H_aux.
             apply Qplus_le_compat; try solve [ apply Qle_refl ].
             destruct H_wf; assumption.
         assert (H_cc_aux2: abs_r a * S i + abs_b0 a <= ones_late a i).
           clear H0; clear H2.
           rewrite H_cc_aux1.
           apply (Qle_trans
             (abs_r a * S i + abs_b0 a)
             (cg(abs_r a * S i + abs_b0 a))
             0).
           destruct (cg_def_linear (abs_r a * S i + abs_b0 a)); assumption.
           apply Zle_impl_Qle.
           apply Zge_le.
           assumption.

         rewrite red_ones_late.
         case_eq (abs_r a * S i + abs_b0 a ?= ones_late a i);
           try solve [ intro H_cmp; apply inj_eq; assumption].
         intro H_cmp.
         rewrite <- Qgt_alt in H_cmp.
         absurd (ones_late a i < abs_r a * S i + abs_b0 a); auto.
         apply Qle_not_lt.
         assumption.

       intro H_tmp; destruct H_tmp.
       elim (Zmin_spec (S i) (cg (abs_r a * (S i) + abs_b0 a))).
         intro H_tmp; destruct H_tmp.
         rewrite H0 in *.
         rewrite H2 in *.
         assert (H_cc_aux1: ones_late a i = i).
           rewrite IHi.
           apply Zeq_impl_nat_eq.
           rewrite ones_late_alt_remove_Zabs_nat.
           rewrite Zmin_left.
           rewrite Zmax_right.
           trivial.
           apply inj_le.
           auto with arith.
           apply Zlt_impl_Zle.
           apply (Zlt_le_trans
             i
             (S i)
             (cg (abs_r a * i + abs_b0 a) + 1)).
             apply inj_lt.
             auto with arith.
             rewrite <- cg_plus_int_rewrite.
             apply (Zle_trans
               (S i)
               (cg (abs_r a * S i + abs_b0 a))
               (cg (abs_r a * i + abs_b0 a + 1))); auto.
             apply cg_monotone_linear.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               abs_r a * (i + 1) + abs_b0 a ==
               abs_r a * i + abs_b0 a + abs_r a).
               ring.
             rewrite H_aux; clear H_aux.
             apply Qplus_le_compat; try solve [ apply Qle_refl ].
             destruct H_wf; assumption.

         assert (H_cc_aux2: abs_r a * S i + abs_b0 a > ones_late a i).
           rewrite H_cc_aux1.
           apply (Qle_lt_trans
             i
             (cg (abs_r a * S i + abs_b0 a) - 1)%Z
             (abs_r a * S i + abs_b0 a));
           try solve [ elim (cg_def_linear (abs_r a * S i + abs_b0 a));
                       intros; assumption ].
           assert (H_aux:
             (cg (abs_r a * S i + abs_b0 a) - 1%nat) ==
             (cg (abs_r a * S i + abs_b0 a) - 1%nat)%Z).
             unfold Qeq; simpl; omega.
           rewrite <- H_aux; clear H_aux.
           unfold Qminus.
           rewrite -> Qle_minus_iff.
           assert (H_aux:
             cg (abs_r a * S i + abs_b0 a) + - (1) + - i ==
             cg (abs_r a * S i + abs_b0 a) + - (i + 1)).
             ring.
           rewrite H_aux; clear H_aux.
           rewrite n_plus_1_eq_S_n.
           rewrite <- Qle_minus_iff.
           apply Zle_impl_Qle.
           assumption.

         rewrite red_ones_late.
         simpl in H_cc_aux2.
         rewrite Qgt_alt in H_cc_aux2.
         rewrite H_cc_aux2.
         rewrite H_cc_aux1.
         reflexivity.

         intro H_tmp; destruct H_tmp.
         rewrite H0 in *.
         rewrite H2 in *.
         clear H2 H0.
         rewrite ones_late_eq_ones_w_late.
         case_eq (w_late a (S i)).
           intro H_w_late.
           rewrite ones_S_i_eq_S_ones_i; auto.
           rewrite <- ones_late_eq_ones_w_late.
           rewrite IHi.
           assert (H_aux: (Z_of_nat (1 + ones_late_alt a i)) = (1 + ones_late_alt a i)%Z).
             apply inj_plus.
           rewrite H_aux; clear H_aux.
           assert (H_cmp: abs_r a * S i + abs_b0 a > ones_late a i).
             rewrite Qlt_alt.
             case_eq (abs_r a * S i + abs_b0 a ?= ones_late a i);
              try solve [
               intro H_cmp;
               simpl in H_w_late;
               rewrite H_cmp in H_w_late;
               rewrite <- beq_nat_refl in H_w_late;
               simpl in H_w_late;
               congruence].
             rewrite <- Qlt_alt.
             rewrite <- Qgt_alt.
             trivial.

           rewrite IHi in H_cmp.
           apply Zle_antisym.
             assert (TH_aux: forall (x: nat) (y: Z), (x < y)%Z -> (1%nat + x <= y)%Z).
               intros x y H_lt.
               replace (1%nat + x)%Z with (- ( -(1) + - x))%Z by ring.
               apply Zle_0_minus_le.
               unfold Zminus.
               rewrite Zopp_involutive.
               rewrite Zplus_assoc.
               apply Zlt_left.
               assumption.
             apply TH_aux; auto.
             apply Qlt_impl_Zlt.
             apply
               (Qlt_le_trans
                 (ones_late_alt a i)
                 (abs_r a * S i + abs_b0 a)
                 (cg (abs_r a * S i + abs_b0 a))); auto.
             elim (cg_def_linear (abs_r a * S i + abs_b0 a)); auto.

             rewrite ones_late_alt_remove_Zabs_nat.
             rewrite Zmin_right; auto.
               rewrite Zmax_right.
                 rewrite Zplus_comm.
                 rewrite <- cg_plus_int_rewrite.
                 apply cg_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   abs_r a * (i + 1) + abs_b0 a ==
                   abs_r a * i + abs_b0 a + abs_r a).
                   ring.
                 rewrite H_aux; clear H_aux.
                 apply Qplus_le_compat; try solve [apply Qle_refl].
                 replace 1%Z with (Z_of_nat 1); auto.
                 destruct H_wf; auto.

                 apply Zlt_impl_Zle.
                 apply
                   (Zlt_le_trans
                     0%nat
                     (cg (abs_r a * S i + abs_b0 a))
                     (cg (abs_r a * i + abs_b0 a) + 1%nat)); auto.
                 rewrite <- cg_plus_int_rewrite.
                 apply cg_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   abs_r a * (i + 1) + abs_b0 a ==
                   abs_r a * i + abs_b0 a + abs_r a).
                   ring.
                 rewrite H_aux; clear H_aux.
                 apply Qplus_le_compat; try solve [apply Qle_refl].
                 destruct H_wf; auto.

               apply
                 (Zge_trans
                   i
                   (cg (abs_r a * S i + abs_b0 a))
                   (cg (abs_r a * i + abs_b0 a))).
                 assert (TH_aux: forall (x: nat) (y: Z), (S x > y)%Z -> (x >= y)%Z).
                   intros x y H_gt.
                   apply Zgt_impl_Zge.
                   assert (H_aux: (x + 1%nat)%Z = S x).
                     assert (H_aux: (Z_of_nat (x + 1%nat)%nat = (x + 1%nat)%Z)%Z).
                       apply inj_plus.
                     rewrite <- H_aux; clear H_aux.
                     rewrite plus_comm.
                     simpl.
                     reflexivity.
                   rewrite H_aux; clear H_aux.
                   assumption.
                 apply TH_aux; auto.
                 apply Zle_ge.
                 apply cg_monotone_linear.
                 apply Qplus_le_compat; try solve [ apply Qle_refl ].
                 rewrite Qmult_comm.
                 assert (H_aux: abs_r a * S i == S i * abs_r a).
                   ring.
                 rewrite H_aux; clear H_aux.
                 apply Qmult_le_compat_r; try solve [ apply le_impl_Qle; auto].
                 destruct H_wf; auto.

           intro H_w_late.
           rewrite ones_S_i_eq_ones_i; auto.
           rewrite <- ones_late_eq_ones_w_late.
           rewrite IHi.
           assert (H_cmp: abs_r a * S i + abs_b0 a <= ones_late a i).
             rewrite Qge_alt.
             case_eq (abs_r a * S i + abs_b0 a ?= ones_late a i).
               intro H_cmp.
               rewrite <- Qeq_alt in H_cmp.
               intro H_cmp'.
               rewrite <- Qlt_alt in H_cmp'.
               rewrite H_cmp in H_cmp'.
               absurd (ones_late a i < ones_late a i); auto.
               apply Qle_not_lt.
               apply Qle_refl.
               intro H_cmp.
               rewrite <- Qlt_alt in H_cmp.
               intro H_cmp'.
               rewrite <- Qlt_alt in H_cmp'.
               absurd (ones_late a i < abs_r a * S i + abs_b0 a); auto.
               apply Qle_not_lt.
               apply Qlt_le_weak.
               assumption.
               intro H_cmp.
               simpl in H_w_late.
               rewrite H_cmp in H_w_late.
               rewrite S_n_nbeq_n in H_w_late.
               simpl in H_w_late.
               congruence.
           rewrite IHi in H_cmp.
           apply Zle_antisym.
             rewrite ones_late_alt_remove_Zabs_nat.
             rewrite Zmin_right; auto.
               rewrite Zmax_right.
                 apply cg_monotone_linear.
                 assert (H_aux:
                   abs_r a * i + abs_b0 a ==
                   abs_r a * i + abs_b0 a + 0).
                   ring.
                 rewrite H_aux; clear H_aux.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   abs_r a * (i + 1) + abs_b0 a ==
                   abs_r a * i + abs_b0 a + abs_r a).
                   ring.
                 rewrite H_aux; clear H_aux.
                 apply Qplus_le_compat; try solve [apply Qle_refl].
                 destruct H_wf; assumption.

                 apply Zlt_impl_Zle.
                 apply
                   (Zlt_le_trans
                     0%nat
                     (cg (abs_r a * S i + abs_b0 a))
                     (cg (abs_r a * i + abs_b0 a) + 1%nat)); auto.
                 rewrite <- cg_plus_int_rewrite.
                 apply cg_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   abs_r a * (i + 1) + abs_b0 a ==
                   abs_r a * i + abs_b0 a + abs_r a).
                   ring.
                 rewrite H_aux; clear H_aux.
                 apply Qplus_le_compat; try solve [apply Qle_refl].
                 destruct H_wf; auto.

               apply
                 (Zge_trans
                   i
                   (cg (abs_r a * S i + abs_b0 a))
                   (cg (abs_r a * i + abs_b0 a))).
                 assert (TH_aux: forall (x: nat) (y: Z), (S x > y)%Z -> (x >= y)%Z).
                   intros x y H_gt.
                   apply Zgt_impl_Zge.
                   assert (H_aux: (x + 1%nat)%Z = S x).
                     assert (H_aux: (Z_of_nat (x + 1%nat)%nat = (x + 1%nat)%Z)%Z).
                       apply inj_plus.
                     rewrite <- H_aux; clear H_aux.
                     rewrite plus_comm.
                     simpl.
                     reflexivity.
                   rewrite H_aux; clear H_aux.
                   assumption.
                 apply TH_aux; auto.
                 apply Zle_ge.
                 apply cg_monotone_linear.
                 apply Qplus_le_compat; try solve [ apply Qle_refl ].
                 rewrite Qmult_comm.
                 assert (H_aux: abs_r a * S i == S i * abs_r a).
                   ring.
                 rewrite H_aux; clear H_aux.
                 apply Qmult_le_compat_r; try solve [ apply le_impl_Qle; auto].
                 destruct H_wf; auto.

             rewrite <- Zge_iff_le.
             apply n_ge_cg_linear.
             assumption.
  Qed.

  Lemma w_early_S_i_eq_true_impl_ones_early_S_i_le_a:
    forall a i,
    forall H_w: w_early a (S i) = true,
    ones (w_early a) (S i) <= (abs_r a * S i + abs_b1 a).
  Proof.
    intros.
    assert (H_w_i: (ones (w_early a) (S i) = S (ones (w_early a) i))%nat).
      apply ones_S_i_eq_S_ones_i; auto.
    simpl in H_w.
    case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
      intro H_cmp.
      rewrite <- Qeq_alt in H_cmp.
      rewrite ones_early_eq_ones_w_early in H_cmp.
      rewrite <- H_cmp.
      rewrite H_w_i.
      apply Qle_refl.

      intro H_cmp.
      rewrite <- Qlt_alt in H_cmp.
      rewrite ones_early_eq_ones_w_early in H_cmp.
      apply Qlt_le_weak.
      rewrite H_w_i.
      assumption.

      intro H_cmp.
      rewrite H_cmp in H_w.
      rewrite <- beq_nat_refl in H_w.
      simpl in H_w.
      congruence.
  Qed.

  Lemma w_early_S_i_eq_false_impl_ones_early_i_gt_a:
    forall a i,
    forall H_w: w_early a (S i) = false,
    S (ones (w_early a) i) > (abs_r a * S i + abs_b1 a).
  Proof.
    intros.
    simpl in H_w.
    case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
      intro H_cmp.
      rewrite H_cmp in H_w.
      rewrite S_n_nbeq_n in H_w.
      simpl in H_w.
      congruence.

      intro H_cmp.
      rewrite H_cmp in H_w.
      rewrite S_n_nbeq_n in H_w.
      simpl in H_w.
      congruence.

      intro H_cmp.
      clear H_w.
      rewrite <- Qgt_alt in H_cmp.
      rewrite ones_early_eq_ones_w_early in H_cmp.
      assumption.
  Qed.

  Property ones_w_le_ones_early:
    forall w: ibw,
    forall a: abstraction_phd,
    forall H_wf_a: well_formed_abstraction_phd a,
    forall H_w_in_a: in_abstraction_phd w a,
    forall i: nat,
    (ones w i <= ones_early a i)%nat.
  Proof.
    intros.
    case_eq i.
      intro H_i.
      simpl.
      apply le_refl.

      intros i' H_i.
      clear H_i i.
      induction i'.
        case_eq (w 1%nat).
        intro H_w.
        assert (H_1_ge_1: (1 >= 1)%nat);
          auto.
        pose (H_w_in_a_1:= H_w_in_a 1%nat H_1_ge_1).
        elim H_w_in_a_1. intros H_aux_true H_aux_false.
        generalize (H_aux_true H_w).
        clear H_1_ge_1 H_w_in_a_1 H_aux_true H_aux_false.
        intro H_ones_le_a.
        simpl in H_ones_le_a.
        simpl.
        rewrite H_w.
        simpl.
        case_eq (1%nat ?= abs_r a * 1%nat + abs_b1 a);
          try solve [ intros; apply le_refl ].
        intros H_cmp.
        rewrite <- Qgt_alt in H_cmp.
        absurd (abs_r a * 1 + abs_b1 a < 1); auto.
        apply Qle_not_lt.
        rewrite H_w in H_ones_le_a.
        assumption.

        intro H_w.
        assert (H_1_ge_1: (1 >= 1)%nat);
          auto.
        pose (H_w_in_a_1:= H_w_in_a 1%nat H_1_ge_1).
        elim H_w_in_a_1. intros H_aux_true H_aux_false.
        generalize (H_aux_false H_w).
        clear H_1_ge_1 H_w_in_a_1 H_aux_true H_aux_false.
        intro H_ones_ge_a.
        simpl in H_ones_ge_a.
        simpl in H_ones_ge_a.

        simpl.
        rewrite H_w.
        simpl.
        case_eq (1%nat ?= abs_r a * 1%nat + abs_b1 a);
          try solve [ intros; unfold Q_of_nat, Qle; simpl; auto with zarith ].

      case_eq (w (S (S i'))).
        intro H_w.
        rewrite ones_S_i_eq_S_ones_i; auto.
        change ((1 + ones w (S i'))%nat) with (S (ones w (S i'))).

        elim (le_lt_eq_dec (ones w (S i')) (ones_early a (S i'))); try omega.
          intro H_cmp.
          apply
            (le_trans
              (S (ones w (S i')))
              (ones_early a (S i'))
              (ones_early a (S (S i')))); try omega.

            assert (H_aux:
              (ones_early a (S (S i'))
               =
               match S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a with
               | Eq => S (ones_early a (S i'))
               | Lt => S (ones_early a (S i'))
               | Gt => ones_early a (S i')
               end)%nat).
               simpl.
              reflexivity.
            rewrite H_aux; clear H_aux.
            case_eq (S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a);
              try omega.

            intro H_cmp.
            rewrite H_cmp.
            assert (H_S_S_i'_ge_1: (S (S i') >= 1)%nat);
              auto with arith.
            pose (H_tmp:= H_w_in_a (S (S i')) H_S_S_i'_ge_1).
            destruct H_tmp.
            generalize (H H_w).
            clear H_S_S_i'_ge_1 H H0 IHi'.
            intro H_ones_le_a.
            assert (H_aux:
              (ones_early a (S (S i'))
               =
               match S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a with
               | Eq => S (ones_early a (S i'))
               | Lt => S (ones_early a (S i'))
               | Gt => ones_early a (S i')
               end)%nat).
               simpl.
              reflexivity.
            rewrite H_aux; clear H_aux.
            case_eq (S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a);
              try omega.
            intro H_cmp'.
            rewrite <- Qgt_alt in H_cmp'.
            absurd (abs_r a * S (S i') + abs_b1 a < S (ones_early a (S i'))); auto.
            apply Qle_not_lt.
            rewrite ones_S_i_eq_S_ones_i in H_ones_le_a; auto.
            rewrite H_cmp in H_ones_le_a.
            assumption.

        intro H_w.
        rewrite ones_S_i_eq_ones_i; auto.
        assert (H_aux:
          (ones_early a (S (S i'))
           =
           match S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a with
           | Eq => S (ones_early a (S i'))
           | Lt => S (ones_early a (S i'))
           | Gt => ones_early a (S i')
           end)%nat).
           simpl.
          reflexivity.
        rewrite H_aux; clear H_aux.
        case_eq (S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a);
        omega.
  Qed.

  Property ones_late_le_ones_w:
    forall w: ibw,
    forall a: abstraction_phd,
    forall H_wf_a: well_formed_abstraction_phd a,
    forall H_w_in_a: in_abstraction_phd w a,
    forall i: nat,
    (ones_late a i <= ones w i)%nat.
  Proof.
    intros.
    case_eq i.
      intro H_i.
      simpl.
      apply le_refl.

      intros i' H_i.
      clear H_i i.
      induction i'.
        case_eq (w 1%nat).
        intro H_w.
        assert (H_1_ge_1: (1 >= 1)%nat);
          auto.
        pose (H_w_in_a_1:= H_w_in_a 1%nat H_1_ge_1).
        elim H_w_in_a_1. intros H_aux_true H_aux_false.
        generalize (H_aux_true H_w).
        clear H_1_ge_1 H_w_in_a_1 H_aux_true H_aux_false.
        intro H_ones_le_a.
        simpl in H_ones_le_a.
        simpl.
        rewrite H_w.
        simpl.
        case_eq (abs_r a * 1%nat + abs_b0 a ?= 0%nat);
          try solve [ auto; intros; apply le_refl ].

        intro H_w.
        assert (H_1_ge_1: (1 >= 1)%nat);
          auto.
        pose (H_w_in_a_1:= H_w_in_a 1%nat H_1_ge_1).
        elim H_w_in_a_1. intros H_aux_true H_aux_false.
        generalize (H_aux_false H_w).
        clear H_1_ge_1 H_w_in_a_1 H_aux_true H_aux_false.
        intro H_ones_ge_a.
        simpl in H_ones_ge_a.

        simpl.
        rewrite H_w.
        simpl.
        case_eq (abs_r a * 1%nat + abs_b0 a ?= 0%nat);
          try solve [ auto; intros; unfold Q_of_nat, Qle; simpl; auto with zarith ].
        intros H_cmp.
        rewrite <- Qgt_alt in H_cmp.
        absurd (0 < abs_r a * 1 + abs_b0 a); auto.
        apply Qle_not_lt.
        rewrite H_w in H_ones_ge_a.
        assumption.

      case_eq (w (S (S i'))).
        intro H_w.
        rewrite ones_S_i_eq_S_ones_i; auto.
        change ((1 + ones w (S i'))%nat) with (S (ones w (S i'))).

        rewrite red_ones_late.
        case_eq (abs_r a * S (S i') + abs_b0 a ?= ones_late a (S i')); omega.

        intro H_w.
        rewrite ones_S_i_eq_ones_i; auto.

        rewrite red_ones_late.
        case_eq (abs_r a * S (S i') + abs_b0 a ?= ones_late a (S i'));
         try omega.
        rewrite <- Qgt_alt.
        intro H_cmp.
        apply lt_le_S.
        apply Qlt_impl_lt.
        apply
          (Qlt_le_trans
            (ones_late a (S i'))
            (abs_r a * S (S i') + abs_b0 a)
            (ones w (S i')));
          try solve [ exact H_cmp ].
        unfold in_abstraction_phd in H_w_in_a.
        rewrite <- ones_S_i_eq_ones_i; auto.
        apply (H_w_in_a (S (S i'))); auto with arith.
  Qed.

  Lemma ones_early_opt_impl_ones_early:
   forall a: abstraction_phd,
   forall i,
   forall (H_ones_early_opt:
     exists v,
     ones_early_opt a i = Some v),
   ones_early_opt a i = Some (ones_early a i).
  Proof.
    intros.
    induction i.
      simpl.
      reflexivity.

      simpl.
      assert (IH_pre: exists v : nat, ones_early_opt a i = Some v).
        elim H_ones_early_opt.
        intros v_S_i H_ones_S_i.
        simpl in H_ones_S_i.
        case_eq (ones_early_opt a i).
          intros v_i H_ones_i.
          exists v_i.
          reflexivity.
          intros H_ones_i.
          rewrite H_ones_i in H_ones_S_i.
          congruence.

      rewrite IHi; auto.
      case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a);
        try reflexivity.
        intro H_cmp.
        case_eq (abs_r a * S i + abs_b0 a ?= ones_early a i);
          try reflexivity.
          intro H_cmp'.
          absurd (exists v : nat, ones_early_opt a (S i) = Some v);
            auto.
          unfold Logic.not.
          intro H_tmp.
          elim H_tmp; clear H_tmp.
          intro v.
          simpl.
          rewrite IHi; auto.
          rewrite H_cmp.
          rewrite H_cmp'.
          congruence.
Qed.

  Lemma ones_late_opt_impl_ones_late:
   forall a: abstraction_phd,
   forall i,
   forall (H_ones_late_opt:
     exists v,
     ones_late_opt a i = Some v),
   ones_late_opt a i = Some (ones_late a i).
  Proof.
    intros.
    induction i.
      simpl.
      reflexivity.

      simpl.
      assert (IH_pre: exists v : nat, ones_late_opt a i = Some v).
        elim H_ones_late_opt.
        intros v_S_i H_ones_S_i.
        simpl in H_ones_S_i.
        case_eq (ones_late_opt a i).
          intros v_i H_ones_i.
          exists v_i.
          reflexivity.
          intros H_ones_i.
          rewrite H_ones_i in H_ones_S_i.
          congruence.

      rewrite IHi; auto.
      case_eq (abs_r a * S i + abs_b0 a ?= ones_late a i);
        try reflexivity.
        intro H_cmp.
        case_eq (S (ones_late a i) ?= abs_r a * S i + abs_b1 a);
          try reflexivity.
          intro H_cmp'.
          absurd (exists v : nat, ones_late_opt a (S i) = Some v);
            auto.
          unfold Logic.not.
          intro H_tmp.
          elim H_tmp; clear H_tmp.
          intro v.
          simpl.
          rewrite IHi; auto.
          rewrite H_cmp.
          rewrite H_cmp'.
          congruence.
  Qed.

  Property ones_late_eq_ones_early:
    forall a: abstraction_phd,
    forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
    forall H_abs_b1_lt_abs_b0: abs_b1 a - abs_b0 a < 1,
    forall i,
    ones_late a i = ones_early a i.
  Proof.
    induction i.
      simpl.
      reflexivity.

      simpl.
      case_eq (abs_r a * S i + abs_b0 a ?= ones_late a i).
        intros H_cmp_zero.
        rewrite IHi.
        case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
          intros H_cmp_one.
          rewrite <- Qeq_alt in *.
          rewrite IHi in H_cmp_zero.
          rewrite <- n_plus_1_eq_S_n in H_cmp_one.
          rewrite <- H_cmp_zero in H_cmp_one.

          absurd (abs_r a * S i + abs_b1 a == abs_r a * S i + abs_b0 a + 1);
            try solve [rewrite H_cmp_one; apply Qeq_refl].
          apply Qlt_not_eq.
          rewrite <- Qplus_assoc.
          apply Qplus_lt_compat_l.
          apply <- Qlt_minus_iff.
          assert (H_aux:
            abs_b0 a + 1 + - abs_b1 a == 1 + - (abs_b1 a - abs_b0 a)).
            ring.
          rewrite H_aux; clear H_aux.
          apply -> Qlt_minus_iff.
          assumption.

          intros H_cmp_one.
          rewrite <- Qeq_alt in *.
          rewrite <- Qlt_alt in *.
          absurd (S (ones_early a i) < abs_r a * S i + abs_b1 a);
            auto.
          rewrite IHi in H_cmp_zero.
          apply Qle_not_lt.
          rewrite <- (n_plus_1_eq_S_n (ones_early a i)).
          rewrite <- H_cmp_zero.
          rewrite <- Qplus_assoc.
          apply Qplus_le_compat; try solve [apply Qle_refl; auto].
          apply Qlt_le_weak.
          apply <- Qlt_minus_iff.
          assert (H_aux:
            abs_b0 a + 1 + - abs_b1 a == 1 + - (abs_b1 a - abs_b0 a)).
            ring.
          rewrite H_aux; clear H_aux.
          apply -> Qlt_minus_iff.
          assumption.

          reflexivity.

        intros H_cmp_zero.
        rewrite IHi.
        case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
          intros H_cmp_one.
          rewrite <- Qeq_alt in H_cmp_one.
          rewrite <- Qlt_alt in H_cmp_zero.
          rewrite IHi in H_cmp_zero.
          assert (H_aux:
            ones_early a i == abs_r a * S i + abs_b1 a - 1).
            rewrite <- H_cmp_one.
            rewrite <- n_plus_1_eq_S_n.
            ring.
          rewrite H_aux in H_cmp_zero; clear H_aux.
          absurd (abs_r a * S i + abs_b0 a < abs_r a * S i + abs_b1 a - 1);
            auto.
          apply Qle_not_lt.
          unfold Qminus.
          rewrite <- Qplus_assoc.
          apply Qplus_le_compat; try solve [apply Qle_refl; auto].
          apply Qlt_le_weak.
          apply <- Qlt_minus_iff.
          assert (H_aux:
            abs_b0 a + - (abs_b1 a + - (1)) == 1 + - (abs_b1 a - abs_b0 a)).
            ring.
          rewrite H_aux; clear H_aux.
          apply -> Qlt_minus_iff.
          assumption.

          intros H_cmp_one.
          rewrite <- Qlt_alt in *.
          absurd (abs_r a * S i + abs_b0 a < abs_r a * S i + abs_b1 a - 1).
            apply Qle_not_lt.
            unfold Qminus.
            rewrite <- Qplus_assoc.
            apply Qplus_le_compat; try solve [apply Qle_refl; auto].
            apply Qlt_le_weak.
            apply <- Qlt_minus_iff.
            assert (H_aux:
              abs_b0 a + - (abs_b1 a + - (1)) == 1 + - (abs_b1 a - abs_b0 a)).
              ring.
            rewrite H_aux; clear H_aux.
            apply -> Qlt_minus_iff.
            assumption.

            rewrite IHi in H_cmp_zero.
            apply
              (Qlt_trans
                (abs_r a * S i + abs_b0 a)
                (ones_early a i)
                (abs_r a * S i + abs_b1 a - 1)); auto.
            apply -> (Qlt_plus 1%nat).
            rewrite Qplus_comm.
            rewrite n_plus_1_eq_S_n.
            assert (H_aux:
              1 + (abs_r a * S i + abs_b1 a - 1) == abs_r a * S i + abs_b1 a).
              ring.
            rewrite H_aux; clear H_aux.
            assumption.

          reflexivity.

        intros H_cmp_zero.
        rewrite IHi.
        case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
          intros H_cmp_one.
          reflexivity.

          intros H_cmp_one.
          reflexivity.

          intros H_cmp_one.
          pose (H_non_empty_S_i:= H_non_empty (S i)).
          simpl in H_non_empty_S_i.
          rewrite H_cmp_one in H_non_empty_S_i.
          rewrite H_cmp_zero in H_non_empty_S_i.
          rewrite IHi in H_non_empty_S_i.
          absurd ((S (ones_early a i) <= ones_early a i)%nat); auto.
          apply lt_not_le.
          auto with arith.
  Qed.

  Property ones_late_le_ones_early_impl_early_in_a:
    forall a: abstraction_phd,
    forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
    in_abstraction_phd (w_early a) a.
  Proof.
    intros.
    unfold in_abstraction_phd.
    intros.
    case_eq i.
      intros H_i.
      rewrite H_i in H_i_ge_1.
      absurd ((0 >= 1)%nat); auto.
      unfold ge.
      auto with arith.

      intros i' H_i.
      rewrite H_i in H_i_ge_1.
      clear H_i i.
      split.
        intro H_w_early_S_i'.
        apply w_early_S_i_eq_true_impl_ones_early_S_i_le_a.
        exact H_w_early_S_i'.

        intro H_w_early_S_i'.
        assert (H_cmp: (abs_r a * S i' + abs_b1 a) < S (ones_early a i')).
          rewrite ones_early_eq_ones_w_early.
          apply w_early_S_i_eq_false_impl_ones_early_i_gt_a; auto.
        pose (H_non_empty_i:=H_non_empty (S i')).
        simpl in H_non_empty_i.
        rewrite Qgt_alt in H_cmp.
        rewrite H_cmp in H_non_empty_i.
        case_eq (abs_r a * S i' + abs_b0 a ?= ones_late a i').
          intro H_cmp'.
          rewrite <- Qeq_alt in H_cmp'.
          rewrite H_cmp'.
          apply le_impl_Qle.
          simpl.
          rewrite H_cmp.
          rewrite <- beq_nat_refl.
          simpl.
          rewrite <- ones_early_eq_ones_w_early.
          apply H_non_empty.

          intro H_cmp'.
          rewrite <- Qlt_alt in H_cmp'.
          simpl.
          rewrite <- ones_early_eq_ones_w_early.
          rewrite H_cmp.
          rewrite <- beq_nat_refl.
          simpl.
          apply
            (Qle_trans
              (abs_r a * S i' + abs_b0 a)
              (ones_late a i')
              (ones_early a i')).
          apply Qlt_le_weak; assumption.
          apply le_impl_Qle.
          apply H_non_empty.

          intro H_cmp'.
          rewrite H_cmp' in H_non_empty_i.
          assert (H_w_late: w_late a (S i') = true).
            simpl.
            rewrite H_cmp'.
            rewrite S_n_nbeq_n.
            trivial.

          case_eq i'.
            intro H_i'.
            rewrite H_i' in *.
            simpl in *.
            absurd (1 <= 0)%nat; auto with arith.
            intros i'' H_i'.
            rewrite H_i' in *.

            elim (Qlt_le_dec (abs_b1 a - abs_b0 a) 1).
              intro H_one_lt_zero.
              generalize (ones_late_eq_ones_early a H_non_empty H_one_lt_zero).
              intro H_late_eq_early.
              assert (H_late_eq_early':
                forall i : nat, ones (w_late a) i = ones (w_early a) i).
                intros.
                rewrite <- ones_late_eq_ones_w_late.
                rewrite <- ones_early_eq_ones_w_early.
                apply H_late_eq_early.
              assert (H_wf_early: well_formed_ibw (w_early a)).
                apply w_early_well_formed.
              assert (H_wf_late: well_formed_ibw (w_late a)).
                apply w_late_well_formed.
              generalize (ones_eq_impl_w_eq _ _ H_late_eq_early').
              intro H_w.
              absurd (w_late a (S (S i'')) = w_early a (S (S i''))); auto.
              rewrite H_w_late, H_w_early_S_i'.
              discriminate.

              intro H_zero_lt_one.
              rewrite <- Qgt_alt in *.
              replace (pred (S (S i''))) with (S i''); auto.
              rewrite <- ones_early_eq_ones_w_early.
              apply
                (Qle_trans
                  (abs_r a * S (S i'') + abs_b0 a)
                  (abs_r a * S (S i'') + (abs_b1 a - 1))
                  (ones_early a (S (S i'')))).
                apply Qplus_le_compat; try solve [apply Qle_refl].
                rewrite Qle_minus_iff.
                assert (H_aux:
                  abs_b1 a - 1 + - abs_b0 a == abs_b1 a - abs_b0 a + - (1)).
                  ring.
                rewrite H_aux; clear H_aux.
                rewrite <- Qle_minus_iff.
                assumption.

                rewrite ones_early_eq_ones_w_early.
                rewrite ones_S_i_eq_ones_i; auto.
                rewrite <- ones_early_eq_ones_w_early.
                apply Qlt_le_weak.
                rewrite Qlt_minus_iff.
                assert (H_aux:
                  ones_early a (S i'') + - (abs_r a * S (S i'') + (abs_b1 a - 1)) ==
                  ones_early a (S i'') + 1 + - (abs_r a * S (S i'') + abs_b1 a)).
                  ring.
                rewrite H_aux; clear H_aux.
                rewrite <- Qlt_minus_iff.
                rewrite n_plus_1_eq_S_n.
                assumption.
  Qed.

  Property ones_late_le_ones_early_impl_late_in_a:
    forall a: abstraction_phd,
    forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
    in_abstraction_phd (w_late a) a.
  Proof.
    intros.
    unfold in_abstraction_phd.
    intros.
    case_eq i.
      intros H_i.
      rewrite H_i in H_i_ge_1.
      absurd ((0 >= 1)%nat); auto.
      unfold ge.
      auto with arith.

      intros i' H_i.
      rewrite H_i in H_i_ge_1.
      clear H_i i.
      split.
        intro H_w.
        simpl in H_w.
        case_eq (abs_r a * S i' + abs_b0 a ?= ones_late a i').
          intro H_cmp.
          rewrite H_cmp in H_w.
          rewrite <- beq_nat_refl in H_w.
          simpl in H_w.
          congruence.

          intro H_cmp.
          rewrite H_cmp in H_w.
          rewrite <- beq_nat_refl in H_w.
          simpl in H_w.
          congruence.

          intro H_cmp.
          rewrite H_cmp in H_w.
          simpl.
          pose (H_non_empty_i:=H_non_empty (S i')).
          simpl in H_non_empty_i.
          rewrite H_cmp in H_non_empty_i.
          case_eq (S (ones_early a i') ?= abs_r a * S i' + abs_b1 a).
            intro H_cmp'.
            rewrite H_cmp' in *.
            rewrite <- Qeq_alt in H_cmp'.
            rewrite <- H_cmp'.
            rewrite <- ones_late_eq_ones_w_late.
            apply le_impl_Qle.
            apply le_lt_n_Sm in H_non_empty_i.
            rewrite H_cmp.
            rewrite S_n_nbeq_n.
            simpl.
            auto with arith.

            intro H_cmp'.
            rewrite H_cmp' in H_non_empty_i.
            rewrite <- Qlt_alt in H_cmp'.
            simpl.
            rewrite <- ones_late_eq_ones_w_late.
            rewrite H_cmp.
            rewrite S_n_nbeq_n.
            simpl.
            apply (Qle_trans
                (S (ones_late a i'))
                (S (ones_early a i'))
                (abs_r a * S i' + abs_b1 a));
              try solve [apply Qlt_le_weak; auto].
            apply le_impl_Qle.
            auto with arith.

            intro H_cmp'.
            rewrite H_cmp' in H_non_empty_i.
            rewrite <- Qgt_alt in *.
            rewrite <- ones_late_eq_ones_w_late.
            elim (Qlt_le_dec (abs_b1 a - abs_b0 a) 1).
              intro H_b1_lt_b0.
              generalize (ones_late_eq_ones_early a H_non_empty H_b1_lt_b0 i').
              intro H_late_eq_early.
              rewrite H_late_eq_early in H_non_empty_i.
              absurd ((S (ones_early a i') <= ones_early a i')%nat); auto.
              apply lt_not_le.
              auto.

              intro H_b0_le_b1.
              rewrite Qgt_alt in H_cmp.
              rewrite H_cmp.
              rewrite <- Qgt_alt in H_cmp.
              rewrite S_n_nbeq_n.
              simpl.
              apply (Qle_trans
                (S (ones_late a i'))
                (abs_r a * S i' + abs_b0 a + 1)
                (abs_r a * S i' + abs_b1 a)).
                rewrite <- n_plus_1_eq_S_n.
                apply Qplus_le_compat; try solve [ apply Qle_refl ].
                apply Qlt_le_weak.
                assumption.
                rewrite <- Qplus_assoc.
                apply Qplus_le_compat; try solve [ apply Qle_refl ].
                apply <- Qle_minus_iff.
                assert (H_aux:
                  abs_b1 a + - (abs_b0 a + 1) == abs_b1 a - abs_b0 a + - (1)).
                  ring.
                rewrite H_aux; clear H_aux.
                apply -> Qle_minus_iff.
                assumption.

        intro H_w.
        simpl.
        simpl in H_w.
        rewrite <- ones_late_eq_ones_w_late.
        case_eq (abs_r a * S i' + abs_b0 a ?= ones_late a i').
          intro H_cmp.
          rewrite <- Qeq_alt in H_cmp.
          rewrite H_cmp.
          rewrite <- beq_nat_refl.
          simpl.
          apply Qle_refl.

          intro H_cmp.
          rewrite <- Qlt_alt in H_cmp.
          apply Qlt_le_weak.
          rewrite <- beq_nat_refl.
          simpl.
          assumption.

          intro H_cmp.
          rewrite H_cmp in H_w.
          rewrite S_n_nbeq_n in H_w.
          simpl in H_w.
          congruence.
  Qed.

  Property non_empty_impl_ones_late_le_ones_early:
    forall a: abstraction_phd,
    forall H_wf: well_formed_abstraction_phd a,
    forall H_non_empty: non_empty a,
    forall i,
    (ones_late a i <= ones_early a i)%nat.
  Proof.
    intros.
    elim H_non_empty.
    intros w H_w_in_a.
    apply
      (le_trans
        (ones_late a i)
        (ones w i)
        (ones_early a i)).
      apply ones_late_le_ones_w; auto.
      apply ones_w_le_ones_early; auto.
  Qed.

  Property early_in_abs:
    forall a: abstraction_phd,
    forall H_wf: well_formed_abstraction_phd a,
    forall H_non_empty: non_empty a,
    in_abstraction_phd (w_early a) a.
  Proof.
    intros.
    apply ones_late_le_ones_early_impl_early_in_a.
    intros.
    apply non_empty_impl_ones_late_le_ones_early; auto.
  Qed.

  Property late_in_abs:
    forall a: abstraction_phd,
    forall H_wf: well_formed_abstraction_phd a,
    forall H_non_empty: non_empty a,
    in_abstraction_phd (w_late a) a.
  Proof.
    intros.
    apply ones_late_le_ones_early_impl_late_in_a.
    intros.
    apply non_empty_impl_ones_late_le_ones_early; auto.
  Qed.

  Property ones_early_rewrite:
    forall a1 a2,
    forall H_wf_a1: well_formed_abstraction_phd a1,
    forall H_wf_a2: well_formed_abstraction_phd a2,
    abs_equal a1 a2 ->
    forall i, (ones_early a1 i = ones_early a2 i).
  Proof.
    intros a1 a2 H_wf_a1 H_wf_a2 H_a1_eq_a2 i.
    destruct H_a1_eq_a2 as [H_r [H_b1 H_b0]].
    repeat rewrite ones_early_eq_ones_early_alt; auto.
    repeat unfold ones_early_alt.
    rewrite H_r.
    rewrite H_b1.
    reflexivity.
  Qed.

  Property ones_late_rewrite:
    forall a1 a2,
    forall H_wf_a1: well_formed_abstraction_phd a1,
    forall H_wf_a2: well_formed_abstraction_phd a2,
    abs_equal a1 a2 ->
    forall i, (ones_late a1 i = ones_late a2 i).
  Proof.
    intros a1 a2 H_wf_a1 H_wf_a2 H_a1_eq_a2 i.
    destruct H_a1_eq_a2 as [H_r [H_b1 H_b0]].
    repeat rewrite ones_late_eq_ones_late_alt; auto.
    repeat unfold ones_late_alt.
    rewrite H_r.
    rewrite H_b0.
    reflexivity.
  Qed.

  Property exists_i_st_ones_early_eq_r_i_plus_b:
    forall a: abstraction_phd,
    forall H_swf_a: strong_well_formed_abstraction_phd a,
    exists i: nat,
      (fl (abs_r a * i + abs_b1 a) = (ones_early a i)%Z)%Z.
  Proof.
    intros.
    elim (Qlt_le_dec (abs_b1 a) 0).
      intro H_b1.
      elim (Qeq_dec (abs_r a) (0)).
        intro H_r_eq_0.
        destruct H_swf_a as [ H_wf_a [ H_b0_b1 [ H_r_impl_b1 H_r_impl_b0 ] ] ].
        absurd (abs_b1 a < 0); auto.
        apply Qle_not_lt.
        apply (Qle_trans _ (abs_b0 a) _); auto.

        intro H_r_diff_0.
        pose (i := Zabs_nat (cg (- abs_b1 a / abs_r a))).
        assert (zi: Z_of_nat i = cg (- abs_b1 a / abs_r a)).
          unfold i.
          rewrite inj_Zabs_nat.
          apply Zabs_eq.
          apply Qle_impl_Zle.
          apply (Qle_trans _ (- abs_b1 a / abs_r a) _);
            try solve [ eapply cg_def_linear ].
          apply Qle_shift_div_l.
          elim (Q_dec (abs_r a) 0); auto.
            intro H; elim H; auto; clear H; intro H_absurd.
            absurd (abs_r a < 0); auto.
            apply Qle_not_lt.
            eapply H_swf_a.
            intro H_absurd.
            absurd (abs_r a == 0); auto.
            assert (H_aux: Z0 * abs_r a == - 0).
              ring.
            rewrite H_aux; clear H_aux.
            apply Qopp_le_compat.
            apply Qlt_le_weak.
            exact H_b1.
        exists i.
        rewrite ones_early_eq_ones_early_alt; try solve [ eapply H_swf_a ].
        rewrite ones_early_alt_remove_Zabs_nat.
        elim (Zmin_spec i (fl (abs_r a * i + abs_b1 a))).
          intros [H_min H_aux].
          rewrite H_aux in *; clear H_aux.
          elim (Z_le_lt_eq_dec i (fl (abs_r a * i + abs_b1 a))); auto.
            intro H_i.
            absurd ((i < fl (abs_r a * i + abs_b1 a))%Z); auto.
            clear H_i H_min.
            apply Zle_not_lt.
            apply Qle_impl_Zle.
            apply (Qle_trans _
              (abs_r a * i + abs_b1 a) _);
            try solve [elim (fl_def (abs_r a * i + abs_b1 a)); auto].
            apply <- Qle_minus_iff.
            assert (H_aux:
              i + - (abs_r a * i + abs_b1 a) == (1 - abs_r a) * i + - abs_b1 a).
              ring.
            rewrite H_aux; clear H_aux.
            apply (Qle_trans _ (inject_Z 0 + inject_Z 0) _);
              try solve [ ring_simplify; apply Qle_refl ].
            apply Qplus_le_compat; auto.
              apply Qmult_le_0_compat.
                apply -> Qle_minus_iff.
                eapply H_swf_a.

                apply Zle_impl_Qle.
                omega.

              rewrite <- (Qopp_involutive Z0).
              apply Qopp_le_compat.
              apply Qlt_le_weak.
              exact H_b1.

            intro H_i.
            rewrite H_i.
            assert (H_aux:
              Zmax O (fl (abs_r a * i + abs_b1 a)) = fl (abs_r a * i + abs_b1 a));
            try solve [ rewrite H_aux; reflexivity ].
            apply Zmax_right.
            apply n_le_fl_linear.
            rewrite <- (Qopp_involutive (abs_b1 a)).
            apply -> Qle_minus_iff.
            unfold Q_of_nat.
            rewrite zi.
            apply (Qle_trans _
              (abs_r a * (- abs_b1 a / abs_r a)) _).
              rewrite Qmult_div_r; auto.
              apply Qle_refl.
              apply Qmult_le_compat_l; try solve [ eapply H_swf_a ].
              eapply cg_def_linear.

          intros [H_min H_aux].
          rewrite H_aux in *; clear H_aux.
          assert (H_aux:
            Zmax O (fl (abs_r a * i + abs_b1 a)) = fl (abs_r a * i + abs_b1 a));
          try solve [ rewrite H_aux; reflexivity ].
          apply Zmax_right.
          apply n_le_fl_linear.
          rewrite <- (Qopp_involutive (abs_b1 a)).
          apply -> Qle_minus_iff.
          unfold Q_of_nat.
          rewrite zi.
          apply (Qle_trans _
            (abs_r a * (- abs_b1 a / abs_r a)) _).
            rewrite Qmult_div_r; auto.
            apply Qle_refl.
            apply Qmult_le_compat_l; try solve [ eapply H_swf_a ].
            eapply cg_def_linear.

      intro H_b1.
      elim (Qeq_dec (abs_r a) (1)).
        intro H_r_eq_1.
        elim (Qle_lt_or_eq 0 (abs_b1 a)); auto.
          intro H_b1'.
          destruct H_swf_a as [ H_wf_a [ H_b0_b1 [ H_r_impl_b1 H_r_impl_b0 ] ] ].
          absurd (0 < abs_b1 a); auto.
          apply Qle_not_lt.
          auto.
          clear H_b1; intro H_b1.
          exists 1%nat.
          rewrite ones_early_eq_ones_early_alt; try solve [ eapply H_swf_a ].
          rewrite ones_early_alt_remove_Zabs_nat.
          repeat rewrite <- H_b1 in *.
          repeat rewrite H_r_eq_1.
          compute.
          reflexivity.

        intro H_r_diff_1.
        pose (i := Zabs_nat (cg (abs_b1 a / (1 - abs_r a)))).
        assert (zi: Z_of_nat i = cg (abs_b1 a / (1 - abs_r a))).
          unfold i.
          rewrite inj_Zabs_nat.
          apply Zabs_eq.
          apply Qle_impl_Zle.
          apply (Qle_trans _ (abs_b1 a / (1 - abs_r a)) _);
            try solve [ eapply cg_def_linear ].
          apply Qle_shift_div_l.
          apply -> Qlt_minus_iff.
          elim (Q_dec (abs_r a) 1); auto.
            intro H; elim H; auto; clear H; intro H_absurd.
            absurd (1 < abs_r a); auto.
            apply Qle_not_lt.
            eapply H_swf_a.
            intro H_absurd.
            absurd (abs_r a == 1); auto.
          ring_simplify.
          eapply H_b1.
        exists i.
        rewrite ones_early_eq_ones_early_alt; try solve [ eapply H_swf_a ].
        rewrite ones_early_alt_remove_Zabs_nat.
        elim (Zmin_spec i (fl (abs_r a * i + abs_b1 a))).
          intros [H_min H_aux].
          rewrite H_aux in *; clear H_aux.
          elim (Z_le_lt_eq_dec i (fl (abs_r a * i + abs_b1 a))); auto.
            intro H_i.
            absurd ((i < fl (abs_r a * i + abs_b1 a))%Z); auto.
            clear H_i H_min.
            apply Zle_not_lt.
            apply Qle_impl_Zle.
            apply (Qle_trans _
              (abs_r a * i + abs_b1 a) _);
            try solve [elim (fl_def (abs_r a * i + abs_b1 a)); auto].
            unfold Q_of_nat.
            repeat rewrite zi.
            apply <- Qle_minus_iff.
            assert (H_aux:
              cg (abs_b1 a / (1 - abs_r a)) +
              - (abs_r a * cg (abs_b1 a / (1 - abs_r a)) + abs_b1 a) ==
              (1 - abs_r a) * cg (abs_b1 a / (1 - abs_r a)) + - abs_b1 a).
              ring.
            rewrite H_aux; clear H_aux.
            apply -> Qle_minus_iff.
            apply (Qle_trans _
              ((1 - abs_r a) * (abs_b1 a / (1 - abs_r a))) _).
              rewrite Qmult_div_r; try solve [ apply Qle_refl ].
              intro H_absurd.
              absurd (abs_r a == 1); auto.
              apply (Qplus_comp (abs_r a) (abs_r a)) in H_absurd;
                try reflexivity.
              ring_simplify in H_absurd.
              rewrite H_absurd.
              reflexivity.

              rewrite Qmult_comm.
              assert (H_aux:
                (1 - abs_r a) * cg (abs_b1 a / (1 - abs_r a)) ==
                cg (abs_b1 a / (1 - abs_r a)) * (1 - abs_r a)).
                rewrite Qmult_comm.
                reflexivity.
              rewrite H_aux; clear H_aux.
              apply Qmult_le_compat_r; try solve [ eapply cg_def_linear ].
              unfold Qminus.
            apply -> Qle_minus_iff.
            eapply H_swf_a.

            intro H_i.
            rewrite H_i.
            assert (H_aux:
              Zmax O (fl (abs_r a * i + abs_b1 a)) = fl (abs_r a * i + abs_b1 a));
            try solve [ rewrite H_aux; reflexivity ].
            apply Zmax_right.
            apply n_le_fl_linear.
            rewrite inj_0.
            apply (Qle_trans _ (inject_Z 0 + inject_Z 0) _);
              try solve [ ring_simplify; apply Qle_refl ].
            apply Qplus_le_compat; auto.
            apply Qmult_le_0_compat.
              eapply H_swf_a.
              apply Zle_impl_Qle.
              unfold i; auto with zarith.

          intros [H_min H_aux].
          rewrite H_aux in *; clear H_aux.
          assert (H_aux:
            Zmax O (fl (abs_r a * i + abs_b1 a)) = fl (abs_r a * i + abs_b1 a));
          try solve [ rewrite H_aux; reflexivity ].
          apply Zmax_right.
          apply n_le_fl_linear.
          rewrite inj_0.
          apply (Qle_trans _ (inject_Z 0 + inject_Z 0) _);
            try solve [ ring_simplify; apply Qle_refl ].
          apply Qplus_le_compat; auto.
          apply Qmult_le_0_compat.
            eapply H_swf_a.
            apply Zle_impl_Qle.
            unfold i; auto with zarith.

  Qed.

  Property exists_i_st_ones_late_eq_r_i_plus_b:
    forall a: abstraction_phd,
    forall H_swf_a: strong_well_formed_abstraction_phd a,
    exists i: nat,
      (cg (abs_r a * i + abs_b0 a) = (ones_late a i)%Z)%Z.
  Proof.
    intros.
    elim (Qlt_le_dec (abs_b0 a) 0).
      intro H_b0.
      elim (Qeq_dec (abs_r a) (0)).
        intro H_r_eq_0.
        destruct H_swf_a as [ H_wf_a [ H_b0_b1 [ H_r_impl_b1 H_r_impl_b0 ] ] ].
        absurd (abs_b0 a < 0); auto.
        apply Qle_not_lt.
        auto.

        intro H_r_diff_0.
        pose (i := Zabs_nat (cg (- abs_b0 a / abs_r a))).
        assert (zi: Z_of_nat i = cg (- abs_b0 a / abs_r a)).
          unfold i.
          rewrite inj_Zabs_nat.
          apply Zabs_eq.
          apply Qle_impl_Zle.
          apply (Qle_trans _ (- abs_b0 a / abs_r a) _);
            try solve [ eapply cg_def_linear ].
          apply Qle_shift_div_l.
          elim (Q_dec (abs_r a) 0); auto.
            intro H; elim H; auto; clear H; intro H_absurd.
            absurd (abs_r a < 0); auto.
            apply Qle_not_lt.
            eapply H_swf_a.
            intro H_absurd.
            absurd (abs_r a == 0); auto.
            assert (H_aux: Z0 * abs_r a == - 0).
              ring.
            rewrite H_aux; clear H_aux.
            apply Qopp_le_compat.
            apply Qlt_le_weak.
            exact H_b0.
        exists i.
        rewrite ones_late_eq_ones_late_alt; try solve [ eapply H_swf_a ].
        rewrite ones_late_alt_remove_Zabs_nat.
        elim (Zmin_spec i (cg (abs_r a * i + abs_b0 a))).
          intros [H_min H_aux].
          rewrite H_aux in *; clear H_aux.
          elim (Z_le_lt_eq_dec i (cg (abs_r a * i + abs_b0 a))); auto.
            intro H_i.
            absurd ((i < cg (abs_r a * i + abs_b0 a))%Z); auto.
            clear H_i H_min.
            apply Zle_not_lt.
            pose (H_aux := (n_ge_cg_linear (abs_r a * i + abs_b0 a) i)).
            apply Zge_le in H_aux; auto; clear H_aux.
            assert (H_aux: i == i + 0); try ring.
            rewrite H_aux at 2; clear H_aux.
            apply Qplus_le_compat; try solve [ apply Qlt_le_weak; eapply H_b0 ].
            assert (H_aux: i == 1 * i); try ring.
            rewrite H_aux at 2; clear H_aux.
            apply Qmult_le_compat_r.
              eapply H_swf_a.
              apply Zle_impl_Qle.
              unfold i; auto with zarith.

            intro H_i.
            rewrite H_i.
            assert (H_aux:
              Zmax O (cg (abs_r a * i + abs_b0 a)) = cg (abs_r a * i + abs_b0 a));
            try solve [ rewrite H_aux; reflexivity ].
            apply Zmax_right.
            apply Qle_impl_Zle.
            apply (Qle_trans _ (abs_r a * i + abs_b0 a) _);
              try solve [ eapply cg_def_linear ].
            rewrite <- (Qopp_involutive (abs_b0 a)).
            apply -> Qle_minus_iff.
            unfold Q_of_nat.
            rewrite zi.
            apply (Qle_trans _
              (abs_r a * (- abs_b0 a / abs_r a)) _).
              rewrite Qmult_div_r; auto.
              apply Qle_refl.
              apply Qmult_le_compat_l; try solve [ eapply H_swf_a ].
              eapply cg_def_linear.

          intros [H_min H_aux].
          rewrite H_aux in *; clear H_aux.
          assert (H_aux:
            Zmax O (cg (abs_r a * i + abs_b0 a)) = cg (abs_r a * i + abs_b0 a));
          try solve [ rewrite H_aux; reflexivity ].
          apply Zmax_right.
          apply Qle_impl_Zle.
          apply (Qle_trans _ (abs_r a * i + abs_b0 a) _);
            try solve [ eapply cg_def_linear ].
          rewrite <- (Qopp_involutive (abs_b0 a)).
          apply -> Qle_minus_iff.
          unfold Q_of_nat.
          rewrite zi.
          apply (Qle_trans _
            (abs_r a * (- abs_b0 a / abs_r a)) _).
            rewrite Qmult_div_r; auto.
            apply Qle_refl.
            apply Qmult_le_compat_l; try solve [ eapply H_swf_a ].
            eapply cg_def_linear.

      intro H_b0.
      elim (Qeq_dec (abs_r a) (1)).
        intro H_r_eq_1.
        elim (Qle_lt_or_eq 0 (abs_b0 a)); auto.
          intro H_b0'.
          destruct H_swf_a as [ H_wf_a [ H_b0_b1 [ H_r_impl_b1 H_r_impl_b0 ] ] ].
          absurd (0 < abs_b0 a); auto.
          apply Qle_not_lt.
          apply (Qle_trans _ (abs_b1 a) _); eauto.
          clear H_b0; intro H_b0.
          exists 1%nat.
          rewrite ones_late_eq_ones_late_alt; try solve [ eapply H_swf_a ].
          rewrite ones_late_alt_remove_Zabs_nat.
          repeat rewrite <- H_b0 in *.
          repeat rewrite H_r_eq_1.
          compute.
          reflexivity.

        intro H_r_diff_1.
        pose (i := Zabs_nat (cg ((abs_b1 a) / (1 - abs_r a)))).
        assert (zi: Z_of_nat i = cg ((abs_b1 a) / (1 - abs_r a))).
          unfold i.
          rewrite inj_Zabs_nat.
          apply Zabs_eq.
          apply Qle_impl_Zle.
          apply (Qle_trans _ ((abs_b1 a) / (1 - abs_r a)) _);
            try solve [ eapply cg_def_linear ].
          apply Qle_shift_div_l.
          apply -> Qlt_minus_iff.
          elim (Q_dec (abs_r a) 1); auto.
            intro H; elim H; auto; clear H; intro H_absurd.
            absurd (1 < abs_r a); auto.
            apply Qle_not_lt.
            eapply H_swf_a.
            intro H_absurd.
            absurd (abs_r a == 1); auto.
          ring_simplify.
          apply (Qle_trans _ (abs_b0 a) _); try solve [ eapply H_swf_a ]; auto.
        exists i.
        rewrite ones_late_eq_ones_late_alt; try solve [ eapply H_swf_a ].
        rewrite ones_late_alt_remove_Zabs_nat.
        elim (Zmin_spec i (cg (abs_r a * i + abs_b0 a))).
          intros [H_min H_aux].
          rewrite H_aux in *; clear H_aux.
          elim (Z_le_lt_eq_dec i (cg (abs_r a * i + abs_b0 a))); auto.
            intro H_i.
            absurd ((i < cg (abs_r a * i + abs_b0 a))%Z); auto.
            clear H_i H_min.
            apply Zle_not_lt.
            apply Qle_impl_Zle.
            apply Zle_impl_Qle.
            pose (H_aux := (n_ge_cg_linear (abs_r a * i + abs_b0 a) i)).
            apply Zge_le in H_aux; auto; clear H_aux.
            apply <- Qle_minus_iff.
            assert (H_aux:
              i + - (abs_r a * i + abs_b0 a) ==
              i * (1 - abs_r a) + - abs_b0 a); try ring.
            rewrite H_aux; clear H_aux.
            apply -> Qle_minus_iff.
            unfold Q_of_nat.
            rewrite zi.
            apply (Qle_trans _
              (((abs_b1 a) / (1 - abs_r a)) * (1 - abs_r a)) _).
              assert (H_aux:
                (abs_b1 a / (1 - abs_r a)) * (1 - abs_r a) == abs_b1 a).
                assert (H_aux:
                  (abs_b1 a / (1 - abs_r a)) * (1 - abs_r a) ==
                  (abs_b1 a * (1 - abs_r a) / (1 - abs_r a))).
                  unfold Qdiv.
                  ring.
                rewrite H_aux; clear H_aux.
                rewrite Qdiv_mult_l; try reflexivity.
                intro H_absurd.
                absurd (abs_r a == 1); auto.
                apply (Qplus_comp (abs_r a) (abs_r a)) in H_absurd;
                  try reflexivity.
                ring_simplify in H_absurd.
                rewrite H_absurd.
                reflexivity.
              rewrite H_aux; clear H_aux.
              eapply H_swf_a.

              apply Qmult_le_compat_r; try solve [eapply cg_def_linear].
              apply -> Qle_minus_iff.
              eapply H_swf_a.

            intro H_i.
            rewrite H_i.
            assert (H_aux:
              Zmax O (cg (abs_r a * i + abs_b0 a)) = cg (abs_r a * i + abs_b0 a));
            try solve [ rewrite H_aux; reflexivity ].
            apply Zmax_right.
            apply Qle_impl_Zle.
            apply (Qle_trans _ (abs_r a * i + abs_b0 a) _);
              try solve [ eapply cg_def_linear ].
            rewrite inj_0.
            apply (Qle_trans _ (inject_Z 0 + inject_Z 0) _);
              try solve [ ring_simplify; apply Qle_refl ].
            apply Qplus_le_compat; auto.
            apply Qmult_le_0_compat.
              eapply H_swf_a.
              apply Zle_impl_Qle.
              unfold i; auto with zarith.

          intros [H_min H_aux].
          rewrite H_aux in *; clear H_aux.
          assert (H_aux:
            Zmax O (cg (abs_r a * i + abs_b0 a)) = cg (abs_r a * i + abs_b0 a));
          try solve [ rewrite H_aux; reflexivity ].
          apply Zmax_right.
          apply Qle_impl_Zle.
          apply (Qle_trans _ (abs_r a * i + abs_b0 a) _);
            try solve [ eapply cg_def_linear ].
          rewrite inj_0.
          apply (Qle_trans _ (inject_Z 0 + inject_Z 0) _);
            try solve [ ring_simplify; apply Qle_refl ].
          apply Qplus_le_compat; auto.
          apply Qmult_le_0_compat.
            eapply H_swf_a.
            apply Zle_impl_Qle.
            unfold i; auto with zarith.

  Qed.

  Lemma ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_S_i_plus_b:
    forall a: abstraction_phd,
    forall H_wf_a: well_formed_abstraction_phd a,
    forall i: nat,
    forall H_early_eq_r_i_plus_b: (fl (abs_r a * i + abs_b1 a) = (ones_early a i)%Z)%Z,
    (fl (abs_r a * S i + abs_b1 a) = (ones_early a (S i))%Z)%Z.
  Proof.
    intros.
    elim (Qeq_dec (abs_r a) 1).
      intro H_r.
      rewrite H_r in *.
      rewrite <- n_plus_1_eq_S_n.
      assert (H_aux:
        1 * (i + 1) + abs_b1 a ==
        1 * i + abs_b1 a + 1); try ring.
      rewrite H_aux; clear H_aux.
      assert (H_aux: (fl (1 * i + abs_b1 a + 1) = fl (1 * i + abs_b1 a) + 1)%Z).
        apply fl_plus_int_rewrite.
      rewrite H_aux; clear H_aux.
      rewrite H_early_eq_r_i_plus_b.
      assert (H_aux: 1%Z = 1%nat); auto.
      rewrite H_aux; clear H_aux.
      rewrite <- inj_plus.
      assert (H_aux: forall n: nat, (n + 1)%nat = S n).
        intro.
        rewrite plus_comm.
        compute.
        reflexivity.
      rewrite H_aux; clear H_aux.

      rewrite red_ones_early.
      case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a);
        try reflexivity.
      intro H_S_early.
      rewrite <- Qgt_alt in H_S_early.
      absurd (abs_r a * S i + abs_b1 a < S (ones_early a i)); auto.
      apply Qle_not_lt.
      rewrite <- n_plus_1_eq_S_n.
      rewrite H_r.
      unfold Q_of_nat.
      rewrite <- H_early_eq_r_i_plus_b.
      apply (Qle_trans _ ((1 * i + abs_b1 a) + 1) _);
        [apply Qplus_le_compat;
          [ eapply fl_def; apply Qle_refl| apply Qle_refl ] |].
      ring_simplify.
      assert (H_aux: i + abs_b1 a + 1 == abs_b1 a + (i + 1));
        [ring|].
      rewrite H_aux; clear H_aux.
      rewrite n_plus_1_eq_S_n.
      apply Qle_refl.

      intro H_r.

      assert (H_max: (0 <= fl (abs_r a * S i + abs_b1 a))%Z).
        apply (Zle_trans _ (fl (abs_r a * i + abs_b1 a)) _).
          rewrite H_early_eq_r_i_plus_b.
          rewrite <- inj_0.
          apply inj_le.
          auto with arith.

          apply fl_monotone_linear.
          rewrite <- n_plus_1_eq_S_n.
          assert (H_aux:
            abs_r a * (i + 1) + abs_b1 a ==
            (abs_r a * i + abs_b1 a) + abs_r a).
            ring.
          rewrite H_aux; clear H_aux.
          rewrite <- (Qplus_0_r (abs_r a * i + abs_b1 a)) at 1.
          apply Qplus_le_compat; [ apply Qle_refl | apply H_wf_a ].

      assert (H_min: (fl (abs_r a * S i + abs_b1 a) <= S i)%Z).
        assert (H_aux: (fl (abs_r a + S i) = S i)%Z).
          unfold Q_of_nat.
          rewrite fl_plus_int_rewrite.
          rewrite <- Zplus_0_l.
          apply Zplus_eq_compat; try reflexivity.
          apply fl_eq_0; try solve [ eapply H_wf_a ].
          elim (Q_dec (abs_r a) 1); auto.
          intro H_aux; elim H_aux; auto.
            intro H_absurd.
            absurd (1 < abs_r a); auto.
            apply Qle_not_lt.
            eapply H_wf_a.
            intro H_absurd.
            absurd (abs_r a == 1); auto.
        unfold Q_of_nat; rewrite <- H_aux at 2; clear H_aux.
        apply fl_monotone_linear.
        apply <- Qle_minus_iff.
        assert (H_aux:
          abs_r a + S i + - (abs_r a * S i + abs_b1 a) ==
          S i + - (abs_r a * (S i - 1) + abs_b1 a)); try ring.
        rewrite H_aux; clear H_aux.
        repeat rewrite <- n_plus_1_eq_S_n.
        assert (H_aux: i + 1 - 1 == i); try ring.
        rewrite H_aux; clear H_aux.
        apply -> Qle_minus_iff.
        apply (Qle_trans _ (fl (abs_r a * i + abs_b1 a) + 1) _);
          try solve [ apply Qlt_le_weak; eapply fl_def ].
        apply Qplus_le_compat; try solve [ apply Qle_refl ].
        rewrite H_early_eq_r_i_plus_b.
        rewrite ones_early_eq_ones_w_early.
        apply Zle_impl_Qle.
        apply inj_le.
        apply ones_i_le_i.

      rewrite ones_early_eq_ones_early_alt; auto.
      rewrite ones_early_alt_remove_Zabs_nat.
      rewrite Zmin_right;
        try solve [ apply Zle_ge; assumption ].
      rewrite Zmax_right; auto.

  Qed.

  Lemma ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_S_i_plus_b:
    forall a: abstraction_phd,
    forall H_wf_a: well_formed_abstraction_phd a,
    forall i: nat,
    forall H_late_eq_r_i_plus_b: (cg (abs_r a * i + abs_b0 a) = (ones_late a i)%Z)%Z,
    (cg (abs_r a * S i + abs_b0 a) = (ones_late a (S i))%Z)%Z.
  Proof.
    intros.

    assert (H_max: (0 <= cg (abs_r a * S i + abs_b0 a))%Z).
      apply (Zle_trans _ (cg (abs_r a * i + abs_b0 a)) _).
        rewrite H_late_eq_r_i_plus_b.
        rewrite <- inj_0.
        apply inj_le.
        auto with arith.

        apply cg_monotone_linear.
        rewrite <- n_plus_1_eq_S_n.
        assert (H_aux:
          abs_r a * (i + 1) + abs_b0 a ==
          (abs_r a * i + abs_b0 a) + abs_r a).
          ring.
        rewrite H_aux; clear H_aux.
        rewrite <- (Qplus_0_r (abs_r a * i + abs_b0 a)) at 1.
        apply Qplus_le_compat; [ apply Qle_refl | apply H_wf_a ].

    assert (H_min: (cg (abs_r a * S i + abs_b0 a) <= S i)%Z).
      pose (H_aux := (n_ge_cg_linear (abs_r a * S i + abs_b0 a) (S i))).
      apply Zge_le in H_aux; auto; clear H_aux.
      assert (H_aux: inject_Z (Z_of_nat (S i)) = Q_of_nat (S i));
        [ unfold Q_of_nat; reflexivity |].
      rewrite H_aux; clear H_aux.
      rewrite <- n_plus_1_eq_S_n.
      assert (H_aux:
        abs_r a * (i + 1) + abs_b0 a ==
        abs_r a * i + abs_b0 a + abs_r a); [ring |].
      rewrite H_aux; clear H_aux.
      apply Qplus_le_compat; [| eapply H_wf_a ].
      apply (Qle_trans _ (cg (abs_r a * i + abs_b0 a)) _);
        [ eapply cg_def_linear |].
      rewrite H_late_eq_r_i_plus_b.
      rewrite ones_late_eq_ones_w_late.
      apply Zle_impl_Qle.
      apply inj_le.
      apply ones_i_le_i.

    rewrite ones_late_eq_ones_late_alt; auto.
    rewrite ones_late_alt_remove_Zabs_nat.
    rewrite Zmin_right;
      try solve [ apply Zle_ge; assumption ].
    rewrite Zmax_right; auto.
  Qed.

  Lemma ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i_plus_x_plus_b:
    forall a: abstraction_phd,
    forall H_wf_a: well_formed_abstraction_phd a,
    forall i: nat,
    forall H_early_eq_r_i_plus_b: (fl (abs_r a * i + abs_b1 a) = (ones_early a i)%Z)%Z,
    forall x: nat,
    (fl (abs_r a * (x + i)%nat + abs_b1 a) = (ones_early a (x + i)%nat)%Z)%Z.
  Proof.
    intros.
    induction x.
      rewrite plus_0_l.
      assumption.

      assert (H_aux: ((S x + i)%nat = S (x + i))%nat); auto with arith.
      rewrite H_aux; clear H_aux.
      apply ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_S_i_plus_b; auto.
  Qed.

  Lemma ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i_plus_x_plus_b:
    forall a: abstraction_phd,
    forall H_wf_a: well_formed_abstraction_phd a,
    forall i: nat,
    forall H_late_eq_r_i_plus_b: (cg (abs_r a * i + abs_b0 a) = (ones_late a i)%Z)%Z,
    forall x: nat,
    (cg (abs_r a * (x + i)%nat + abs_b0 a) = (ones_late a (x + i)%nat)%Z)%Z.
  Proof.
    intros.
    induction x.
      rewrite plus_0_l.
      assumption.

      assert (H_aux: ((S x + i)%nat = S (x + i))%nat); auto with arith.
      rewrite H_aux; clear H_aux.
      apply ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_S_i_plus_b; auto.
  Qed.

  Property ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i'_plus_b:
    forall a: abstraction_phd,
    forall H_wf_a: well_formed_abstraction_phd a,
    forall i: nat,
    forall H_early_eq_r_i_plus_b: (fl (abs_r a * i + abs_b1 a) = (ones_early a i)%Z)%Z,
    forall i': nat,
    forall H_i_le_i': (i <= i')%nat,
    (fl (abs_r a * i' + abs_b1 a) = (ones_early a i')%Z)%Z.
  Proof.
    intros.
    case_eq i'.
      intro H_i'.
      case_eq i.
        intro H_i.
        rewrite H_i in H_early_eq_r_i_plus_b.
        rewrite H_early_eq_r_i_plus_b.
        reflexivity.

        intros i0 H_i.
        rewrite H_i' in H_i_le_i'.
        rewrite H_i in H_i_le_i'.
        absurd (S i0 <= O)%nat; auto with arith.

      intros i0' H_i'.
      rewrite H_i' in *.
      assert (H_aux: exists x:nat, (i' = (x + i)%nat)%nat).
        exists (S i0' - i)%nat.
        omega.
      elim H_aux; clear H_aux.
      intros x H_x.
      rewrite <- H_i'.
      rewrite H_x.
      apply ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i_plus_x_plus_b;
        auto.
  Qed.

  Property ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i'_plus_b:
    forall a: abstraction_phd,
    forall H_wf_a: well_formed_abstraction_phd a,
    forall i: nat,
    forall H_late_eq_r_i_plus_b: (cg (abs_r a * i + abs_b0 a) = (ones_late a i)%Z)%Z,
    forall i': nat,
    forall H_i_le_i': (i <= i')%nat,
    (cg (abs_r a * i' + abs_b0 a) = (ones_late a i')%Z)%Z.
  Proof.
    intros.
    case_eq i'.
      intro H_i'.
      case_eq i.
        intro H_i.
        rewrite H_i in H_late_eq_r_i_plus_b.
        rewrite H_late_eq_r_i_plus_b.
        reflexivity.

        intros i0 H_i.
        rewrite H_i' in H_i_le_i'.
        rewrite H_i in H_i_le_i'.
        absurd (S i0 <= O)%nat; auto with arith.

      intros i0' H_i'.
      rewrite H_i' in *.
      assert (H_aux: exists x:nat, (i' = (x + i)%nat)%nat).
        exists (S i0' - i)%nat.
        omega.
      elim H_aux; clear H_aux.
      intros x H_x.
      rewrite <- H_i'.
      rewrite H_x.
      apply ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i_plus_x_plus_b;
        auto.
  Qed.

  Lemma exists_i_st_ones_early_and_ones_late_eq_r_i_plus_b:
    forall a: abstraction_phd,
    forall H_swf_a: strong_well_formed_abstraction_phd a,
    exists i: nat,
      (fl (abs_r a * i + abs_b1 a) = (ones_early a i)%Z)%Z
      /\
      (cg (abs_r a * i + abs_b0 a) = (ones_late a i)%Z)%Z.
  Proof.
    intros.
    elim (exists_i_st_ones_early_eq_r_i_plus_b H_swf_a).
    intros i1 H_early.
    elim (exists_i_st_ones_late_eq_r_i_plus_b H_swf_a).
    intros i2 H_late.
    pose (i := Max.max i1 i2).
    exists i.
    split.
      destruct H_swf_a as [ H_wf_a H_wf_a_aux ].
      apply (ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i'_plus_b H_wf_a H_early).
      apply Max.le_max_l.

      destruct H_swf_a as [ H_wf_a H_wf_a_aux ].
      apply (ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i'_plus_b H_wf_a H_late).
      apply Max.le_max_r.
  Qed.

  Lemma exists_i_st_ones_early1_and_ones_late2_eq_r_i_plus_b:
    forall a1 a2: abstraction_phd,
    forall H_swf_a1: strong_well_formed_abstraction_phd a1,
    forall H_swf_a2: strong_well_formed_abstraction_phd a2,
    exists i: nat,
      (fl (abs_r a1 * i + abs_b1 a1) = (ones_early a1 i)%Z)%Z
      /\
      (cg (abs_r a2 * i + abs_b0 a2) = (ones_late a2 i)%Z)%Z.
  Proof.
    intros.
    elim (exists_i_st_ones_early_eq_r_i_plus_b H_swf_a1).
    intros i1 H_early1.
    elim (exists_i_st_ones_late_eq_r_i_plus_b H_swf_a2).
    intros i2 H_late2.
    pose (i := Max.max i1 i2).
    exists i.
    split.
      destruct H_swf_a1 as [ H_wf_a1 H_wf_a1_aux ].
      apply (ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i'_plus_b H_wf_a1 H_early1).
      apply Max.le_max_l.

      destruct H_swf_a2 as [ H_wf_a2 H_wf_a2_aux ].
      apply (ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i'_plus_b H_wf_a2 H_late2).
      apply Max.le_max_r.
  Qed.

End early_and_late_properties.

Lemma ones_late_le_ones_early_impl_non_empty:
  forall a,
  forall H_wf: well_formed_abstraction_phd a,
  forall H_early_prec_late: (forall i, ones_late a i <= ones_early a i)%nat,
  non_empty a.
Proof.
  intros.
  unfold non_empty.
  exists (w_early a).
  apply ones_late_le_ones_early_impl_early_in_a; assumption.
Qed.

Section non_empty_test_properties.

  Property non_empty_test_impl_ones_late_le_ones_early_aux:
    forall a,
    forall H_wf: well_formed_abstraction_phd a,


    forall H_non_empty_alt: non_empty_test_alt a,
    forall i,
    (ones_late a i <= ones_early a i)%nat.
  Proof.
    intros.
    destruct H_non_empty_alt as [H_den_b1 H_non_empty].
    rewrite ones_early_eq_ones_early_alt; auto.
    rewrite ones_late_eq_ones_late_alt; auto.
    apply inj_le_rev.
    rewrite ones_early_alt_remove_Zabs_nat.
    rewrite ones_late_alt_remove_Zabs_nat.
    apply Zmax_le_compat_l.
    apply Zmin_le_compat_l.
    assert (H_aux:
      (fl (abs_r a * i + abs_b1 a) =
       fl (Qred (abs_r a * i + abs_b1 a)))%Z).
      apply fl_rewrite.
      rewrite Qred_correct.
      apply Qeq_refl.
    rewrite H_aux; clear H_aux.
    rewrite fl_eq_cg.
    apply cg_monotone_linear.
    apply
      (Qle_trans
        (abs_r a * i + abs_b0 a)
        (abs_r a * i + (abs_b1 a - (1 - (1 # Qden (Qred (abs_r a * i + abs_b1 a))))))
        (Qred (abs_r a * i + abs_b1 a) - (1 - (1 # Qden (Qred (abs_r a * i + abs_b1 a)))))).
      apply Qplus_le_compat; try solve [ apply Qle_refl ].
      apply
        (Qle_trans
          (abs_b0 a)
          (abs_b1 a - (1 - (1 # Qden (abs_r a))))
          (abs_b1 a - (1 - (1 # Qden (Qred (abs_r a * i + abs_b1 a)))))).
        apply <- Qle_minus_iff.
        assert (H_aux:
          abs_b1 a - (1 - (1 # Qden (abs_r a))) + - abs_b0 a ==
          abs_b1 a - abs_b0 a + - (1 - (1 # Qden (abs_r a)))).
          ring.
        rewrite H_aux; clear H_aux.
        apply -> Qle_minus_iff.
        assumption.
        apply Qplus_le_compat; try solve [ apply Qle_refl ].
        apply Qopp_le_compat.
        apply Qplus_le_compat; try solve [ apply Qle_refl ].
        apply Qopp_le_compat.
        apply den_r_le_den_r_i_p_b; auto.

      unfold Qminus.
      rewrite Qplus_assoc.
      apply Qplus_le_compat; try solve [ apply Qle_refl ].
      rewrite Qred_correct.
      apply Qle_refl.
  Qed.

  Lemma simpl_std:
    forall x y: Q,
    ((Qnum x * QDen y)%Z # (Qden x * Qden y)) == x.
  Proof.
    intros.
    unfold Qeq, Qmult, Qdiv; simpl.
    rewrite Zpos_mult_morphism.
    ring.
  Qed.

  Property non_empty_test_equal_compat:
    forall a1 a2: abstraction_phd,
    forall H_a1_eq_a2: abs_equal a1 a2,
    forall H_non_empty1: non_empty_test a1,
    forall H_den:
      1 # Qden (abs_b1 a1) * Qden (abs_r a1) <=
      1 # Qden (abs_b1 a2) * Qden (abs_r a2),
    non_empty_test a2.
  Proof.
    intros.
    unfold non_empty_test in *.
    destruct H_a1_eq_a2 as [H_r [H_b1 H_b0]].
    simpl in *.
    rewrite simpl_std in *.
    rewrite <- H_b0.
    apply
      (Qle_trans
        (1 - (1 # Qden (abs_b1 a2) * Qden (abs_r a2)))
        (1 - (1 # Qden (abs_b1 a1) * Qden (abs_r a1)))
        (abs_b1 a2 - abs_b0 a1)); auto.
      apply Qplus_le_compat; try solve [apply Qle_refl].
      apply Qopp_le_compat.
      assumption.
      rewrite <- H_b1.
      assumption.
  Qed.

  Property abs_equal_abs_std_non_empty:
    forall a: abstraction_phd,
    abs_equal a (abs_std a).
  Proof.
    intros.
    repeat split; auto;
    unfold Qeq; simpl;
    rewrite Zpos_mult_morphism;
    ring.
  Qed.

  Property non_empty_test_impl_ones_late_le_ones_early:
    forall a,
    forall H_wf: well_formed_abstraction_phd a,
    forall H_non_empty: non_empty_test a,
    forall i,
    (ones_late a i <= ones_early a i)%nat.
  Proof.
    intros.
    pose (a_std := abs_std a).
    assert (H_a_eq_a_std: abs_equal a a_std).
      apply abs_equal_abs_std_non_empty.
    assert (H_wf_std: well_formed_abstraction_phd a_std).
      apply (well_formed_abstraction_phd_abs_equal_compat H_a_eq_a_std).
      assumption.
    rewrite (ones_early_rewrite H_wf H_wf_std); auto.
    rewrite (ones_late_rewrite H_wf H_wf_std); auto.
    apply non_empty_test_impl_ones_late_le_ones_early_aux; auto.
    split; auto.
  Qed.

End non_empty_test_properties.


Section on_properties.

  Property on_abs_well_formed_abstraction_phd_compat:
    forall (a1:abstraction_phd) (a2:abstraction_phd),
    forall H_wf_a1: well_formed_abstraction_phd a1,
    forall H_wf_a2: well_formed_abstraction_phd a2,
    well_formed_abstraction_phd (on_abs a1 a2).
  Proof.
    intros.
    unfold well_formed_abstraction_phd.
    simpl.
    destruct H_wf_a1 as [ H_r1_pos H_r1_le_1 ].
    destruct H_wf_a2 as [ H_r2_pos H_r1_le_2 ].
    split.
      apply Qmult_le_0_compat; assumption.
      apply (Qle_trans _ (abs_r a2) _); auto.
      assert (H_aux: abs_r a2 == 1 * abs_r a2); [ring|].
      rewrite H_aux at 2; clear H_aux.
      apply Qmult_le_compat_r; auto.
  Qed.

  Lemma on_w1_w2_le_on_a1_a2:
    forall (w1:ibw) (w2:ibw),
    forall (a1:abstraction_phd) (a2:abstraction_phd),
    forall H_wf_a1: well_formed_abstraction_phd a1,
    forall H_wf_a2: well_formed_abstraction_phd a2,
    forall (H_a1_eq_abs_w1: in_abstraction_phd w1 a1),
    forall (H_a2_eq_abs_w2: in_abstraction_phd w2 a2),
    forall i,
    forall H_i_ge_1: (i >= 1)%nat,
    forall (H_on: on w1 w2 i = true),
    ones (on w1 w2) i <=
    (abs_r a1 * abs_r a2) * i + (abs_b1 a1 * abs_r a2 + abs_b1 a2).
  Proof.
    intros.
    generalize (on_eq_1_impl_w1_eq_1 w1 w2 i H_on).
    intro H_w1.
    generalize (on_eq_1_impl_w2_eq_1 w1 w2 i H_on).
    intro H_w2.
    assert (H_w1_le_a1 : ones w1 i <= abs_r a1 * i + abs_b1 a1).
      unfold in_abstraction_phd in H_a1_eq_abs_w1.
      generalize (H_a1_eq_abs_w1 i H_i_ge_1).
      clear H_a1_eq_abs_w1.
      intro H_aux. elim H_aux. clear H_aux.
      intros H_aux_true H_aux_false. clear H_aux_false.
      generalize (H_aux_true H_w1). clear H_aux_true.
      trivial.

    rewrite ones_on_def.

    assert (H_w2_le_a2:
      ones w2 (ones w1 i) <= (abs_r a2 * ones w1 i + abs_b1 a2)).
      unfold in_abstraction_phd in H_a2_eq_abs_w2.
      assert (H_ones_w1_ge_1: (ones w1 i >= 1)%nat).
        case_eq i.
          intro H_i.
          rewrite H_i in H_i_ge_1.
          absurd ((0 >= 1)%nat); auto.
          unfold ge.
          apply le_Sn_O.

          intros.
          simpl.
          rewrite <- H.
          rewrite H_w1.
          auto with arith.
      generalize (H_a2_eq_abs_w2 (ones w1 i) H_ones_w1_ge_1).
      clear H_a2_eq_abs_w2.
      intro H_aux. elim H_aux. clear H_aux.
      intros H_aux_true H_aux_false. clear H_aux_false.
      generalize (H_aux_true H_w2). clear H_aux_true.
      trivial.


    apply
      (Qle_trans
        (ones w2 (ones w1 i))
        (abs_r a2 * ones w1 i + abs_b1 a2)
        (abs_r a1 * abs_r a2 * i + (abs_b1 a1 * abs_r a2 + abs_b1 a2))
        H_w2_le_a2).
    assert (H_aux:
      abs_r a1 * abs_r a2 * i + (abs_b1 a1 * abs_r a2 + abs_b1 a2) ==
      (abs_r a1 * abs_r a2 * i + abs_b1 a1 * abs_r a2) + abs_b1 a2).
      ring.
    rewrite H_aux; clear H_aux.
    apply Qplus_le_compat; try solve [ apply Qle_refl ].
    assert (H_aux:
      abs_r a1 * abs_r a2 * i + abs_b1 a1 * abs_r a2 ==
      (abs_r a1 * i + abs_b1 a1) * abs_r a2).
      ring.
    rewrite H_aux; clear H_aux.
    rewrite Qmult_comm.
    apply Qmult_le_compat_r; try solve [ apply H_wf_a2 ].
    assumption.
  Qed.

  Lemma on_ge_0:
    forall (w1:ibw) (w2:ibw) i,
    forall (H_on: on w1 w2 i = false),
    (ones (on w1 w2) i >= 0).
  Proof.
    intros.
    assert ((0 <= ones (on w1 w2) i)%nat).
      auto with arith.
    simpl.
    apply (le_impl_Qle H).
  Qed.

  Lemma abs_b0_neg_impl_ones_ge_a:
    forall (w:ibw) (a:abstraction_phd),
    forall H_wf_a: well_formed_abstraction_phd a,
    forall H_flo: abs_b0 a <= 0,
    forall H_a_eq_abs_w: in_abstraction_phd w a,
    forall i:nat,
    ones w i >= abs_r a * i + abs_b0 a.
  Proof.
    induction i.
      assert (H_aux: abs_r a * 0 == 0).
        ring.
      rewrite H_aux; clear H_aux.
      assert (H_aux: 0 + abs_b0 a == abs_b0 a).
        apply Qplus_0_l.
      rewrite H_aux; clear H_aux.
      simpl.
      exact H_flo.

      case_eq (w (S i)).
        intro H_w.
        rewrite ones_S_i_eq_S_ones_i; auto.
        simpl.
        repeat rewrite <- n_plus_1_eq_S_n.
        assert (H_aux:
          abs_r a * (i + 1) + abs_b0 a ==
          abs_r a * i + abs_b0 a + abs_r a).
          ring.
        rewrite H_aux; clear H_aux.
        apply Qplus_le_compat; try solve [ apply H_wf_a ].
        exact IHi.

        intro H_w.
        unfold in_abstraction_phd in H_a_eq_abs_w.
        assert (H_S_i_ge_1:(S i >= 1)%nat).
          auto with arith.
        generalize (H_a_eq_abs_w (S i) H_S_i_ge_1).
        intro H_aux. elim H_aux. clear H_aux.
        intros H_aux_true H_aux_false. clear H_aux_true.
        generalize (H_aux_false H_w). clear H_aux_false.
        intro H_cc.
        simpl in H_cc.
        rewrite H_w in H_cc.
        simpl in H_cc.
        apply
          (Qle_trans
            (abs_r a * S i + abs_b0 a)
            (ones w i)
            (ones w (S i))); auto.
        apply le_impl_Qle.
        apply ones_increasing; auto.
  Qed.

  Lemma on_w1_w2_ge_on_a1_a2:
    forall (w1:ibw) (w2:ibw),
    forall (a1:abstraction_phd) (a2:abstraction_phd),
    forall H_wf_a1: well_formed_abstraction_phd a1,
    forall H_flo_a1: abs_b0 a1 <= 0,
    forall H_wf_a2: well_formed_abstraction_phd a2,
    forall H_flo_a2: abs_b0 a2 <= 0,
    forall (H_a1_eq_abs_w1: in_abstraction_phd w1 a1),
    forall (H_a2_eq_abs_w2: in_abstraction_phd w2 a2),
    forall i,
    forall (H_on: on w1 w2 i = false),
     abs_r a1 * abs_r a2 * i + (abs_b0 a1 * abs_r a2 + abs_b0 a2)
     <= ones (on w1 w2) i.
  Proof.
    intros.
    rewrite ones_on_def.
    generalize (abs_b0_neg_impl_ones_ge_a H_wf_a1 H_flo_a1 H_a1_eq_abs_w1 i).
    intro H_w1_ge_a1.
    generalize (abs_b0_neg_impl_ones_ge_a H_wf_a2 H_flo_a2 H_a2_eq_abs_w2 (ones w1 i)).
    intro H_w2_ge_a2.
    apply
      (Qle_trans
        (abs_r a1 * abs_r a2 * i + (abs_b0 a1 * abs_r a2 + abs_b0 a2))
        (abs_r a2 * ones w1 i + abs_b0 a2)
        (ones w2 (ones w1 i))); auto.
    rewrite Qplus_assoc.
    apply Qplus_le_compat; try solve [ apply Qle_refl ].
    assert (H_r_pos_2: (0 <= abs_r a2)).
      apply H_wf_a2.
    generalize
      (Qmult_le_compat_r
        (abs_r a1 * i + abs_b0 a1)
        (ones w1 i)
        (abs_r a2)
        H_w1_ge_a1
        (H_r_pos_2)).
    intro H_cc.
    rewrite Qmult_plus_distr_l in H_cc.
    assert (H_aux: abs_r a1 * i * abs_r a2 == abs_r a1 * abs_r a2 * i).
      ring.
    rewrite H_aux in H_cc; clear H_aux.
    assert (H_aux: ones w1 i * abs_r a2 == abs_r a2 * ones w1 i).
      ring.
    rewrite H_aux in H_cc; clear H_aux.
    exact H_cc.
  Qed.

  Property on_abs_correctness_aux:
    forall (w1:ibw) (w2:ibw),
    forall (a1:abstraction_phd) (a2:abstraction_phd),
    forall H_wf_a1: well_formed_abstraction_phd a1,
    forall H_wf_a2: well_formed_abstraction_phd a2,
    forall (H_a1_eq_abs_w1: in_abstraction_phd w1 a1),
    forall (H_a2_eq_abs_w2: in_abstraction_phd w2 a2),
    in_abstraction_phd (on w1 w2) (on_abs a1 a2).
  Proof.
    intros.

    assert (H_aux:
      exists a1_0,
        (abs_b1 a1_0 == abs_b1 a1) /\
        (abs_b0 a1_0 == 0) /\
        (abs_r a1_0 == abs_r a1)).
      exists (absmake (abs_b1 a1) 0 (abs_r a1)).
      simpl.
      repeat split; eapply Qeq_refl.
    elim H_aux.
    clear H_aux.
    intros a1_0 H_a1_0.
    assert (H_wf_a1_0: well_formed_abstraction_phd a1_0).
      unfold well_formed_abstraction_phd.
      destruct H_a1_0.
      destruct H0.
      rewrite H1.
      assumption.
    assert (H_abs_b01_0: abs_b0 a1_0 <= 0).
      destruct H_a1_0.
      destruct H0.
      rewrite H0.
      eapply Qle_refl.

    assert (H_aux:
      exists a2_0,
        (abs_b1 a2_0 == abs_b1 a2) /\
        (abs_b0 a2_0 == 0) /\
        (abs_r a2_0 == abs_r a2)).
      exists (absmake (abs_b1 a2) 0 (abs_r a2)).
      simpl.
      repeat split; eapply Qeq_refl.
    elim H_aux.
    clear H_aux.
    intros a2_0 H_a2_0.
    assert (H_wf_a2_0: well_formed_abstraction_phd a2_0).
      unfold well_formed_abstraction_phd.
      destruct H_a2_0.
      destruct H0.
      rewrite H1.
      assumption.
    assert (H_abs_b02_0: abs_b0 a2_0 <= 0).
      destruct H_a2_0.
      destruct H0.
      rewrite H0.
      eapply Qle_refl.

    unfold in_abstraction_phd.
    intros.

    split.
      intro H_on.
      simpl.
      eapply on_w1_w2_le_on_a1_a2; assumption.

      intro H_on.
      elim (Q_dec (abs_b0 a1) 0);
      elim (Q_dec (abs_b0 a2) 0).
      intros H_aux1 H_aux2.
      elim H_aux1;
      elim H_aux2.

        clear H_aux1 H_aux2.
        intros H_abs_b01 H_abs_b02.
        elim (Qlt_alt (abs_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b01).
        clear H_aux1 H_aux2.
        intro H_abs_b01_eq_cmp.
        elim (Qlt_alt (abs_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b02).
        clear H_aux1 H_aux2.
        intro H_abs_b02_eq_cmp.
        simpl.
        rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.
        apply
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 (Qlt_le_weak (abs_b0 a1) 0 H_abs_b01)
            H_wf_a2 (Qlt_le_weak (abs_b0 a2) 0 H_abs_b02)
            H_a1_eq_abs_w1 H_a2_eq_abs_w2);
          auto.

        clear H_aux1 H_aux2.
        intros H_abs_b01 H_abs_b02.
        elim (Qgt_alt (abs_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b01).
        clear H_aux1 H_aux2.
        intro H_abs_b01_eq_cmp.
        elim (Qlt_alt (abs_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b02).
        clear H_aux1 H_aux2.
        intro H_abs_b02_eq_cmp.
        simpl.
        rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.

        assert (H_a1_0_eq_abs_w1: in_abstraction_phd w1 a1_0).
          assert (H_a1_in_a1_0: abs_included_test a1 a1_0).
            apply abs_weakening_0;
            decompose [and] H_a1_0;
            auto.
            rewrite H2; reflexivity.
            rewrite H; reflexivity.
          apply
            (w_in_a1_and_a1_in_a2_impl_w_in_a2
              H_wf_a1 H_wf_a1_0
              H_a1_in_a1_0 H_a1_eq_abs_w1).

        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1_0 H_abs_b01_0
            H_wf_a2 (Qlt_le_weak (abs_b0 a2) 0 H_abs_b02)
            H_a1_0_eq_abs_w1 H_a2_eq_abs_w2
            i H_on).
        decompose [and] H_a1_0.
        rewrite H2, H1.
        trivial.

        clear H_aux1 H_aux2.
        intros H_abs_b01 H_abs_b02.
        elim (Qlt_alt (abs_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b01).
        clear H_aux1 H_aux2.
        intro H_abs_b01_eq_cmp.
        elim (Qgt_alt (abs_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b02).
        clear H_aux1 H_aux2.
        intro H_abs_b02_eq_cmp.
        simpl.
        rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.

        assert (H_a2_0_eq_abs_w2: in_abstraction_phd w2 a2_0).
          assert (H_a2_in_a2_0: abs_included_test a2 a2_0).
            apply abs_weakening_0;
            decompose [and] H_a2_0;
            auto.
            rewrite H2; reflexivity.
            rewrite H; reflexivity.
          apply
            (w_in_a1_and_a1_in_a2_impl_w_in_a2
              H_wf_a2 H_wf_a2_0
              H_a2_in_a2_0 H_a2_eq_abs_w2).

        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 (Qlt_le_weak (abs_b0 a1) 0 H_abs_b01)
            H_wf_a2_0 H_abs_b02_0
            H_a1_eq_abs_w1 H_a2_0_eq_abs_w2
            i H_on).
        decompose [and] H_a2_0.
        rewrite H2, H1.
        trivial.

        clear H_aux1 H_aux2.
        intros H_abs_b01 H_abs_b02.
        elim (Qgt_alt (abs_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b01).
        clear H_aux1 H_aux2.
        intro H_abs_b01_eq_cmp.
        elim (Qgt_alt (abs_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b02).
        clear H_aux1 H_aux2.
        intro H_abs_b02_eq_cmp.
        simpl.
        rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.

        assert (H_a1_0_eq_abs_w1: in_abstraction_phd w1 a1_0).
          assert (H_a1_in_a1_0: abs_included_test a1 a1_0).
            apply abs_weakening_0;
            decompose [and] H_a1_0;
            auto.
            rewrite H2; reflexivity.
            rewrite H; reflexivity.
          apply
            (w_in_a1_and_a1_in_a2_impl_w_in_a2
              H_wf_a1 H_wf_a1_0
              H_a1_in_a1_0 H_a1_eq_abs_w1).

        assert (H_a2_0_eq_abs_w2: in_abstraction_phd w2 a2_0).
          assert (H_a2_in_a2_0: abs_included_test a2 a2_0).
            apply abs_weakening_0;
            decompose [and] H_a2_0;
            auto.
            rewrite H2; reflexivity.
            rewrite H; reflexivity.
          apply
            (w_in_a1_and_a1_in_a2_impl_w_in_a2
              H_wf_a2 H_wf_a2_0
              H_a2_in_a2_0 H_a2_eq_abs_w2).

        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1_0 H_abs_b01_0
            H_wf_a2_0 H_abs_b02_0
            H_a1_0_eq_abs_w1 H_a2_0_eq_abs_w2
            i H_on).
        decompose [and] H_a1_0.
        rewrite H2, H1.
        decompose [and] H_a2_0.
        rewrite H5, H4.
        trivial.

        intros H_abs_b02 H_aux.
        elim H_aux.
        clear H_aux.
        intro H_abs_b01.
        elim (Qlt_alt (abs_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b01).
        clear H_aux1 H_aux2.
        intro H_abs_b01_eq_cmp.
        elim (Qeq_alt (abs_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b02).
        clear H_aux1 H_aux2.
        intro H_abs_b02_eq_cmp.
        simpl.
        rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.
        assert (H_abs_b02_le_0: abs_b0 a2 <= 0).
          rewrite H_abs_b02.
          apply Qle_refl.
        apply
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 (Qlt_le_weak (abs_b0 a1) 0 H_abs_b01)
            H_wf_a2 H_abs_b02_le_0
            H_a1_eq_abs_w1 H_a2_eq_abs_w2);
          auto.

        clear H_aux.
        intro H_abs_b01.
        elim (Qgt_alt (abs_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b01).
        clear H_aux1 H_aux2.
        intro H_abs_b01_eq_cmp.
        elim (Qeq_alt (abs_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b02).
        clear H_aux1 H_aux2.
        intro H_abs_b02_eq_cmp.
        simpl.
        rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.

        assert (H_a1_0_eq_abs_w1: in_abstraction_phd w1 a1_0).
          assert (H_a1_in_a1_0: abs_included_test a1 a1_0).
            apply abs_weakening_0;
            decompose [and] H_a1_0;
            auto.
            rewrite H2; reflexivity.
            rewrite H; reflexivity.
          apply
            (w_in_a1_and_a1_in_a2_impl_w_in_a2
              H_wf_a1 H_wf_a1_0
              H_a1_in_a1_0 H_a1_eq_abs_w1).

        assert (H_abs_b02_le_0: abs_b0 a2 <= 0).
          rewrite H_abs_b02.
          apply Qle_refl.
        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1_0 H_abs_b01_0
            H_wf_a2 H_abs_b02_le_0
            H_a1_0_eq_abs_w1 H_a2_eq_abs_w2
            i H_on).
        decompose [and] H_a1_0.
        rewrite H2, H1.
        trivial.

        intros H_aux H_abs_b01.
        elim H_aux.
        clear H_aux.
        intro H_abs_b02.
        elim (Qeq_alt (abs_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b01).
        clear H_aux1 H_aux2.
        intro H_abs_b01_eq_cmp.
        elim (Qlt_alt (abs_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b02).
        clear H_aux1 H_aux2.
        intro H_abs_b02_eq_cmp.
        simpl.
        rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.
        assert (H_abs_b01_le_0: abs_b0 a1 <= 0).
          rewrite H_abs_b01.
          apply Qle_refl.
        apply
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 H_abs_b01_le_0
            H_wf_a2 (Qlt_le_weak (abs_b0 a2) 0 H_abs_b02)
            H_a1_eq_abs_w1 H_a2_eq_abs_w2);
          auto.

        clear H_aux.
        intro H_abs_b02.
        elim (Qeq_alt (abs_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b01).
        clear H_aux1 H_aux2.
        intro H_abs_b01_eq_cmp.
        elim (Qgt_alt (abs_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b02).
        clear H_aux1 H_aux2.
        intro H_abs_b02_eq_cmp.
        simpl.
        rewrite H_abs_b01_eq_cmp.
        rewrite H_abs_b02_eq_cmp.

        assert (H_a2_0_eq_abs_w2: in_abstraction_phd w2 a2_0).
          assert (H_a2_in_a2_0: abs_included_test a2 a2_0).
            apply abs_weakening_0;
            decompose [and] H_a2_0;
            auto.
            rewrite H2; reflexivity.
            rewrite H; reflexivity.
          apply
            (w_in_a1_and_a1_in_a2_impl_w_in_a2
              H_wf_a2 H_wf_a2_0
              H_a2_in_a2_0 H_a2_eq_abs_w2).

        assert (H_abs_b01_le_0: abs_b0 a1 <= 0).
          rewrite H_abs_b01.
          apply Qle_refl.
        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 H_abs_b01_le_0
            H_wf_a2_0 H_abs_b02_0
            H_a1_eq_abs_w1 H_a2_0_eq_abs_w2
            i H_on).
        decompose [and] H_a2_0.
        rewrite H2, H1.
        trivial.

        intros H_abs_b02 H_abs_b01.
        elim (Qeq_alt (abs_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b01).
        clear H_aux1 H_aux2.
        intro H_abs_b01_eq_cmp.
        elim (Qeq_alt (abs_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_abs_b02).
        clear H_aux1 H_aux2.
        intro H_abs_b02_eq_cmp.
        simpl.
        rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.

        assert (H_abs_b01_le_0: abs_b0 a1 <= 0).
          rewrite H_abs_b01.
          apply Qle_refl.
        assert (H_abs_b02_le_0: abs_b0 a2 <= 0).
          rewrite H_abs_b02.
          apply Qle_refl.
        apply
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 H_abs_b01_le_0
            H_wf_a2 H_abs_b02_le_0
            H_a1_eq_abs_w1 H_a2_eq_abs_w2
            i H_on).
  Qed.

End on_properties.


Section not_properties.

  Property not_abs_correctness_aux:
    forall w: ibw,
    forall a:abstraction_phd,
    forall H_wf_a: well_formed_abstraction_phd a,
    forall H_a_eq_abs_w: in_abstraction_phd w a,
    in_abstraction_phd (not w) (not_abs a).
  Proof.
    intros.
    unfold in_abstraction_phd.
    intros.
    case_eq i.
      intros H_i.
      rewrite H_i in H_i_ge_1.
      absurd ((0 >= 1)%nat); auto.
      unfold ge.
      auto with arith.

      intros i' H_i.
      rewrite H_i in H_i_ge_1.
      clear H_i i.
      induction i'.
        split.
          intro H_not.
          assert (H_w: w 1%nat = false).
            unfold not in H_not.
            assert (H_false_eq_not_true: false = negb true); auto.
            rewrite H_false_eq_not_true; clear H_false_eq_not_true.
            apply negb_sym.
            auto.
          simpl.
          rewrite H_w.
          simpl.
          pose (H_w_1_in_a:= H_a_eq_abs_w 1%nat H_i_ge_1).
          destruct H_w_1_in_a.
          pose (H_cc:= H0 H_w).
          simpl in H_cc.
          rewrite H_w in H_cc.
          simpl in H_cc.
          apply <- Qle_minus_iff.
          assert (H_aux:
            (1 - abs_r a) * 1 + - abs_b0 a + - (1) ==
            0 + - (abs_r a * 1 + abs_b0 a)).
            ring.
          rewrite H_aux; clear H_aux.
          apply -> Qle_minus_iff.
          assumption.

          intro H_not.
          assert (H_w: w 1%nat = true).
            unfold not in H_not.
            assert (H_false_eq_not_true: true = negb false); auto.
            rewrite H_false_eq_not_true; clear H_false_eq_not_true.
            apply negb_sym.
            auto.

          simpl.

          generalize (H_a_eq_abs_w 1%nat H_i_ge_1).
          clear H_a_eq_abs_w.
          intro H_aux. elim H_aux. clear H_aux.
          intros H_aux_true H_aux_false. clear H_aux_false.
          generalize (H_aux_true H_w). clear H_aux_true.
          simpl.
          intro H_abs_b1.

          rewrite H_w in *.
          simpl.
          simpl in H_abs_b1.
          apply <- Qle_minus_iff.
          assert (H_aux:
            0 + - ((1 - abs_r a) * 1 + - abs_b1 a) ==
            abs_r a * 1 + abs_b1 a + - (1)).
            ring.
          rewrite H_aux; clear H_aux.
          apply -> Qle_minus_iff.
          assumption.

        split.
          intro H_not_S_S_i'.
          assert (H_w_S_S_i': w (S (S i')) = false).
            unfold not in H_not_S_S_i'.
            assert (H_false_eq_not_true: false = negb true); auto.
            rewrite H_false_eq_not_true; clear H_false_eq_not_true.
            apply negb_sym.
            auto.

          case_eq (w (S i')).
            intros H_w_S_i'.
            assert (H_not_S_i': not w (S i') = false).
              unfold not.
              rewrite H_w_S_i'.
              simpl.
              trivial.

            rewrite ones_S_i_eq_S_ones_i; auto.
            simpl.
            rewrite H_w_S_i'.
            simpl.

            rewrite ones_not_def.
            rewrite <- n_plus_1_eq_S_n.
            assert (H_aux: (i' - ones w i')%nat == (i' - ones w i')%Q).
              eapply minus_impl_Qminus.
              eapply ones_i_le_i.
            rewrite H_aux; clear H_aux.

            assert (H_ones_w_ge_a: abs_r a * S (S i') + abs_b0 a <= ones w (S (S i'))).
              unfold in_abstraction_phd in H_a_eq_abs_w.
              generalize (H_a_eq_abs_w (S (S i')) H_i_ge_1).
              clear H_a_eq_abs_w.
              intro H_aux. elim H_aux. clear H_aux.
              intros H_aux_true H_aux_false. clear H_aux_true.
              generalize (H_aux_false H_w_S_S_i'). clear H_aux_false.
              trivial.
            rewrite ones_S_i_eq_ones_i in H_ones_w_ge_a; auto.
            rewrite ones_S_i_eq_S_ones_i in H_ones_w_ge_a; auto.
            simpl in H_ones_w_ge_a.
            rewrite <- (n_plus_1_eq_S_n (S i')) in H_ones_w_ge_a.
            rewrite <- (n_plus_1_eq_S_n (ones w i')) in H_ones_w_ge_a.

            rewrite <- n_plus_1_eq_S_n.
            rewrite -> Qle_minus_iff.
            assert (H_aux:
              (1 - abs_r a) * (S i' + 1) + - abs_b0 a + - (i' - ones w i' + 1) ==
              ones w i' + (S i' - i') + - (abs_r a * (S i' + 1) + abs_b0 a)).
              ring.
            rewrite H_aux; clear H_aux.
            rewrite <- Qle_minus_iff.
            assert (H_aux: S i' - i' == 1).
              rewrite <- n_plus_1_eq_S_n.
              ring.
            rewrite H_aux; clear H_aux.
            assumption.

            intros H_w_S_i'.
            assert (H_not_w_S_i': not w (S i') = true).
              unfold not.
              rewrite H_w_S_i'.
              simpl.
              trivial.

            simpl.
            rewrite H_w_S_S_i'.
            rewrite H_w_S_i'.
            simpl.

            assert (H_ones_w_ge_a: abs_r a * S (S i') + abs_b0 a <= ones w (S (S i'))).
              unfold in_abstraction_phd in H_a_eq_abs_w.
              generalize (H_a_eq_abs_w (S (S i')) H_i_ge_1).
              clear H_a_eq_abs_w.
              intro H_aux. elim H_aux. clear H_aux.
              intros H_aux_true H_aux_false. clear H_aux_true.
              generalize (H_aux_false H_w_S_S_i'). clear H_aux_false.
              intro H_cc.
              trivial.
            rewrite ones_S_i_eq_ones_i in H_ones_w_ge_a; auto.
            rewrite ones_S_i_eq_ones_i in H_ones_w_ge_a; auto.

            rewrite ones_not_def.
            rewrite <- n_plus_1_eq_S_n.
            rewrite <- n_plus_1_eq_S_n.
            assert (H_aux: (i' - ones w i')%nat == (i' - ones w i')%Q).
              eapply minus_impl_Qminus.
              eapply ones_i_le_i.
            rewrite H_aux; clear H_aux.

            apply <- Qle_minus_iff.
            assert (H_aux:
              (1 - abs_r a) * S (S i') + - abs_b0 a + - (i' - ones w i' + 1 + 1) ==
              ones w i' + (S (S i') - i' - 1 - 1) + - (abs_r a * S (S i') + abs_b0 a)).
              ring.
            rewrite H_aux; clear H_aux.
            apply -> Qle_minus_iff.
            assert (H_aux: ones w i' + (S (S i') - i' - 1 - 1) == ones w i').
              repeat rewrite <- n_plus_1_eq_S_n.
              ring.
            rewrite H_aux; clear H_aux.
            assumption.

          intro H_not_S_S_i'.
          assert (H_w_S_S_i': w (S (S i')) = true).
            unfold not in H_not_S_S_i'.
            assert (H_false_eq_not_true: true = negb false); auto.
            rewrite H_false_eq_not_true; clear H_false_eq_not_true.
            apply negb_sym.
            auto.

          case_eq (w (S i')).
          intros H_w_S_i'.
          assert (H_not_w_S_i': not w (S i') = false).
            unfold not.
            rewrite H_w_S_i'.
            simpl.
            trivial.

          case_eq (w i').
            intros H_w_i'.
            rewrite ones_S_i_eq_ones_i; auto.
            simpl.
            rewrite H_w_S_i'.
            simpl.
            rewrite ones_not_def.
            assert (H_aux: (i' - ones w i')%nat == (i' - ones w i')%Q).
              eapply minus_impl_Qminus.
              eapply ones_i_le_i.
            rewrite H_aux; clear H_aux.

            assert (H_ones_w_le_a: ones w (S (S i')) <= abs_r a * (S (S i')) + abs_b1 a).
              unfold in_abstraction_phd in H_a_eq_abs_w.
              generalize (H_a_eq_abs_w (S (S i')) H_i_ge_1).
              clear H_a_eq_abs_w.
              intro H_aux. elim H_aux. clear H_aux.
              intros H_aux_true H_aux_false. clear H_aux_false.
              generalize (H_aux_true H_w_S_S_i'). clear H_aux_true.
              trivial.
            rewrite ones_S_i_eq_S_ones_i in H_ones_w_le_a; auto.
            simpl in H_ones_w_le_a.
            rewrite H_w_S_i' in H_ones_w_le_a.
            simpl in H_ones_w_le_a.
            rewrite <- (n_plus_1_eq_S_n (S (ones w i'))) in H_ones_w_le_a.
            rewrite <- (n_plus_1_eq_S_n (ones w i')) in H_ones_w_le_a.

            apply <- Qle_minus_iff.
            assert (H_aux:
              i' - ones w i' + - ((1 - abs_r a) * S (S i') + - abs_b1 a) ==
              abs_r a * S (S i') + abs_b1 a + - (ones w i' + S (S i') + - i')).
              ring.
            rewrite H_aux; clear H_aux.
            apply -> Qle_minus_iff.
            rewrite <- n_plus_1_eq_S_n at 1.
            rewrite <- n_plus_1_eq_S_n.
            assert (H_aux:
              ones w i' + (i' + 1 + 1) + - i' == ones w i' + 1 + 1).
              ring.
            rewrite H_aux; clear H_aux.
            assumption.

            intros H_w_i'.
            case_eq i'.
              intro H_i'.
              rewrite H_i' in *.
              simpl.
              rewrite H_w_S_S_i'.
              rewrite H_w_S_i'.
              simpl.
              simpl in IHi'.
              rewrite H_w_S_i' in IHi'.
              simpl in IHi'.
              pose (H_w_2_in_a:= H_a_eq_abs_w 2).
              simpl in H_w_2_in_a.
              rewrite H_w_S_S_i' in H_w_2_in_a.
              rewrite H_w_S_i' in H_w_2_in_a.
              simpl in H_w_2_in_a.
              assert (H_2_ge_1: (2 >= 1)%nat);
                auto with arith.
              pose (H_tmp:= H_w_2_in_a H_2_ge_1).
              destruct H_tmp as [H_true H_false].

              apply <- Qle_minus_iff.
              assert (H_aux:
                0 + - ((1 - abs_r a) * 2 + - abs_b1 a) ==
                abs_r a * 2 + abs_b1 a + - (2)).
                ring.
              rewrite H_aux; clear H_aux.
              apply -> Qle_minus_iff.
              auto.

              intros i'' H_i''.
              rewrite <- H_i''.
              assert (H_not_w_i: not w i' = true).
                unfold not.
                rewrite H_i''.
                rewrite <- H_i''.
                rewrite H_w_i'.
                simpl.
                trivial.
              rewrite ones_S_i_eq_ones_i; auto.
              simpl.
              rewrite H_w_S_i'.
              simpl.

              rewrite ones_not_def.
              assert (H_aux: (i' - ones w i')%nat == (i' - ones w i')%Q).
                eapply minus_impl_Qminus.
                eapply ones_i_le_i.
              rewrite H_aux; clear H_aux.

              assert (H_ones_w_le_a:
                ones w (S (S i')) <= abs_r a * S (S i') + abs_b1 a).
                unfold in_abstraction_phd in H_a_eq_abs_w.
                generalize (H_a_eq_abs_w (S (S i')) H_i_ge_1).
                clear H_a_eq_abs_w.
        &nb