Library abstraction_hfl_prim_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_hfl_prim_def.

Section Abstractionh_def.

  Definition absh_equal (a1: abstractionh) (a2:abstractionh) :=
    (absh_r a1 == absh_r a2) /\
    (absh_b1 a1) == (absh_b1 a2) /\
    (absh_b0 a1) == (absh_b0 a2).

  Instance absh_equal_is_equiv : Equivalence _ absh_equal.
  Proof.
    constructor ; unfold absh_equal ; red ; intuition.
    transitivity (absh_r y) ; auto.
    transitivity (absh_b1 y) ; auto.
    transitivity (absh_b0 y) ; auto.
  Qed.

End Abstractionh_def.

Definition absh_equiv (a1: abstractionh) (a2:abstractionh) :=
  absh_included a1 a2 /\ absh_included a2 a1.

Definition absh_equiv_test (a1: abstractionh) (a2:abstractionh) :=
  absh_included_test a1 a2 /\ absh_included_test a2 a1.

Section abstraction_equivalence_properties.

  Property absh_included_test_impl_absh_included:
    forall a1 a2: abstractionh,
    forall H_a1_in_test_a2: absh_included_test a1 a2,
    absh_included a1 a2.
  Proof.
    intros.
    unfold absh_included.
    intros.
    unfold in_abstractionh.
    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)
            (absh_r a1 * i + absh_b1 a1)
            (absh_r a1 * i + absh_b1 a2)); auto.
        apply Qplus_le_compat; auto.
        apply Qle_refl.

        intro H_w.
        apply
          (Qle_trans
            (absh_r a1 * i + absh_b0 a2)
            (absh_r a1 * i + absh_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_abstractionh a1,
    forall H_wf_a2: well_formed_abstractionh a2,
    forall H_a1_in_a2: absh_included_test a1 a2,
    forall H_w_in_a1: in_abstractionh w a1,
    in_abstractionh w a2.
  Proof.
    intros.
    unfold in_abstractionh.
    intros i H_i_ge_1.
    split.
      intro H_w.
      unfold in_abstractionh 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)
        (absh_r a1 * i + absh_b1 a1)
        (absh_r a1 * i + absh_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_abstractionh 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
          (absh_r a1 * i + absh_b0 a2)
          (absh_r a1 * i + absh_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 absh_weakening_aux:
    forall a1 a2: abstractionh,
    forall H_one: absh_b1 a1 <= absh_b1 a2,
    forall H_absh_b0: absh_b0 a1 >= absh_b0 a2,
    forall H_r: absh_r a1 == absh_r a2,
    absh_included_test a1 a2.
  Proof.
    intros.
    unfold absh_included_test.
    repeat split; auto.
  Qed.

  Property absh_weakening_0:
    forall a1 a2: abstractionh,
    forall H_absh_b01: absh_b0 a1 > 0,
    forall H_r: absh_r a1 == absh_r a2,
    forall H_one: absh_b1 a1 == absh_b1 a2,
    forall H_absh_b02: absh_b0 a2 == 0,
    absh_included_test a1 a2.
  Proof.
    intros.
    eapply absh_weakening_aux; auto.
    rewrite H_one.
    apply Qle_refl.
    rewrite H_absh_b02.
    eapply Qlt_le_weak.
    assumption.
  Qed.

  Property absh_equal_sym:
    forall a1 a2: abstractionh,
    forall H_a1_eq_a2: absh_equal a1 a2,
    absh_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 absh_equal_impl_absh_included_test:
    forall a1 a2: abstractionh,
    forall H_a1_eq_a2: absh_equal a1 a2,
    absh_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 absh_equal_impl_absh_equiv_test:
    forall a1 a2: abstractionh,
    forall H_a1_eq_a2: absh_equal a1 a2,
    absh_equiv_test a1 a2.
  Proof.
    intros.
    split.
      apply absh_equal_impl_absh_included_test; auto.
      apply absh_equal_impl_absh_included_test; auto.
      apply absh_equal_sym.
      assumption.
  Qed.

  Property absh_equiv_test_impl_absh_equal:
    forall a1 a2: abstractionh,
    forall H_a1_eq_a2: absh_equiv_test a1 a2,
    absh_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_absh_b11_le_absh_b12 H_absh_b02_le_absh_b01.
    elim H_tmp2; clear H_tmp2.
    intros H_r' H_tmp'.
    elim H_tmp'; clear H_tmp' H_r'.
    intros H_absh_b12_le_absh_b11 H_absh_b01_le_absh_b02.
    repeat split.
      trivial.
      apply Qle_antisym; assumption.
      apply Qle_antisym; assumption.
  Qed.

  Property absh_equal_correctness:
    forall a1 a2: abstractionh,
    forall H_wf1: well_formed_abstractionh a1,
    forall H_wf2: well_formed_abstractionh a2,
    forall w: ibw,
    forall H_w_in_a1: in_abstractionh w a1,
    forall H_eq: absh_equal a1 a2,
    in_abstractionh w a2.
  Proof.
    intros.
    apply absh_equal_impl_absh_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_abstractionh_absh_equal_compat:
    forall a1 a2: abstractionh,
    forall H_eq: absh_equal a1 a2,
    forall H_wf1: well_formed_abstractionh a1,
      well_formed_abstractionh a2.
  Proof.
    intros.
    destruct H_eq as [H_r [H_b1 H_b0]].
    unfold well_formed_abstractionh in *.
    rewrite <- H_r.
    assumption.
  Qed.

End abstraction_equivalence_properties.

Fixpoint ones_early_opt (a:abstractionh) (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') (absh_r a * i + absh_b1 a) with
      | Lt | Eq => Some (S ones_i')
      | Gt =>
        match Qcompare (absh_r a * i + absh_b0 a) ones_i' with
        | Lt | Eq => Some (ones_i')
        | _ => None
        end
      end
    end
  end.

Fixpoint ones_late_opt (a:abstractionh) (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 (absh_r a * i + absh_b0 a) ones_i' with
      | Lt | Eq => Some (ones_i')
      | Gt =>
        match Qcompare (S ones_i') (absh_r a * i + absh_b1 a) with
        | Lt | Eq => Some (S ones_i')
        | Gt => None
        end
      end
    end
  end.

Definition non_empty_alt (a: abstractionh) :=
  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') ?= absh_r a * S i' + absh_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 absh_r a * (S i') + absh_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') (absh_r a * S i' + absh_b1 a) with
       | Lt | Eq => Some (S ones_i')
       | Gt =>
         match Qcompare (absh_r a * S i' + absh_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 (absh_r a * S i' + absh_b0 a) ones_i' with
       | Lt | Eq => Some (ones_i')
       | Gt =>
         match Qcompare (S ones_i') (absh_r a * S i' + absh_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:abstractionh,
    forall i,
    ((Z_of_nat (ones_early_alt a i))%Z =
      Zmax O (Zmin i (fl (absh_r a * i + absh_b1 a))))%Z.
  Proof.
    intros.
    unfold ones_early_alt.
    rewrite inj_Zabs_nat.
    elim (Zabs_spec (Zmax O (Zmin i (fl (absh_r a * i + absh_b1 a))))).
      intro H_tmp; destruct H_tmp.
      rewrite H0.
      reflexivity.
      intro H_tmp; destruct H_tmp.
      elim (Zmax_spec O (Zmin i (fl (absh_r a * i + absh_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:abstractionh,
    forall i,
    ((Z_of_nat (ones_late_alt a i))%Z =
      Zmax O (Zmin i (cg (absh_r a * i + absh_b0 a))))%Z.
  Proof.
    intros.
    unfold ones_late_alt.
    rewrite inj_Zabs_nat.
    elim (Zabs_spec (Zmax O (Zmin i (cg (absh_r a * i + absh_b0 a))))).
      intro H_tmp; destruct H_tmp.
      rewrite H0.
      reflexivity.
      intro H_tmp; destruct H_tmp.
      elim (Zmax_spec O (Zmin i (cg (absh_r a * i + absh_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: abstractionh,
    well_formed_ones (ones_early a).
  Proof.
    intros.
    split.
      simpl.
      reflexivity.

      intro.
      simpl.
      case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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: abstractionh,
    well_formed_ones (ones_late a).
  Proof.
    intros.
    split.
      simpl.
      reflexivity.

      intro.
      simpl.
      case_eq (absh_r a * S i + absh_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: abstractionh,
    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 ?= absh_r a * 1%nat + absh_b1 a);
          intros;
          simpl;
          reflexivity.

        assert (H_aux:
          (ones_early a (S (S i'))
           =
           match S (ones_early a (S i')) ?= absh_r a * (S (S i')) + absh_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')) ?= absh_r a * S (S i') + absh_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')) ?= absh_r a * S (S i') + absh_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: abstractionh,
    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 (absh_r a * 1%nat + absh_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 absh_r a * S (S i') + absh_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 (absh_r a * S (S i') + absh_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: abstractionh,
    forall H_wf: well_formed_abstractionh 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 (absh_r a * O%nat + absh_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 (absh_r a * 0%nat + absh_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 (absh_r a * S i + absh_b1 a)))).
       intro H_tmp; destruct H_tmp.
       elim (Zmin_spec (S i) (fl (absh_r a * (S i) + absh_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 (absh_r a * S i + absh_b1 a))
                 (fl (absh_r a * i + absh_b1 a))); auto.
             apply Zle_ge.
             apply fl_monotone_linear.
             assert (H_aux:
               absh_r a * i + absh_b1 a ==
               absh_r a * i + absh_b1 a + 0).
               ring.
             rewrite H_aux; clear H_aux.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               absh_r a * (i + 1) + absh_b1 a ==
               absh_r a * i + absh_b1 a + absh_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 (absh_r a * S i + absh_b1 a))
               (fl (absh_r a * i + absh_b1 a))); auto.
             apply fl_monotone_linear.
             assert (H_aux:
               absh_r a * i + absh_b1 a ==
               absh_r a * i + absh_b1 a + 0).
               ring.
             rewrite H_aux; clear H_aux.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               absh_r a * (i + 1) + absh_b1 a ==
               absh_r a * i + absh_b1 a + absh_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) > absh_r a * S i + absh_b1 a).
           clear H0; clear H2.
           rewrite H_cc_aux1.
           apply (Qlt_le_trans
             (absh_r a * S i + absh_b1 a)
             (fl (absh_r a * S i + absh_b1 a) + 1)
             1).
           destruct (fl_def (absh_r a * S i + absh_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) ?= absh_r a * S i + absh_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) > absh_r a * S i + absh_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) < absh_r a * S i + absh_b1 a); auto.
           apply Qle_not_lt.
           apply Qlt_le_weak.
           assumption.

       intro H_tmp; destruct H_tmp.
       elim (Zmin_spec (S i) (fl (absh_r a * (S i) + absh_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 (absh_r a * i + absh_b1 a) + 1%nat)).
             apply inj_lt.
             auto with arith.
             rewrite <- fl_plus_int_rewrite.
             apply (Zle_trans
               (S i)
               (fl (absh_r a * S i + absh_b1 a))
               (fl (absh_r a * i + absh_b1 a + 1))); auto.
             apply fl_monotone_linear.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               absh_r a * (i + 1) + absh_b1 a ==
               absh_r a * i + absh_b1 a + absh_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) <= absh_r a * S i + absh_b1 a).
           rewrite H_cc_aux1.
           apply (Qle_trans
             (S i)
             (fl (absh_r a * S i + absh_b1 a))
             (absh_r a * S i + absh_b1 a));
             try solve [ elim (fl_def (absh_r a * S i + absh_b1 a)); auto ].
           apply Zle_impl_Qle.
           assumption.
         rewrite red_ones_early.
         case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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) <= absh_r a * S i + absh_b1 a).
             rewrite Qle_alt.
             case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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))
                 (absh_r a * S i + absh_b1 a)
                 (fl (absh_r a * S i + absh_b1 a) + 1)); auto.
             elim (fl_def (absh_r a * S i + absh_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:
                   absh_r a * (i + 1) + absh_b1 a ==
                   absh_r a * i + absh_b1 a + absh_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 (absh_r a * S i + absh_b1 a))
                     (fl (absh_r a * i + absh_b1 a) + 1%nat)); auto.
                 rewrite <- fl_plus_int_rewrite.
                 apply fl_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   absh_r a * (i + 1) + absh_b1 a ==
                   absh_r a * i + absh_b1 a + absh_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 (absh_r a * S i + absh_b1 a))
                   (fl (absh_r a * i + absh_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: absh_r a * S i == S i * absh_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) > absh_r a * S i + absh_b1 a).
             rewrite Qgt_alt.
             case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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:
                   absh_r a * i + absh_b1 a ==
                   absh_r a * i + absh_b1 a + 0).
                   ring.
                 rewrite H_aux; clear H_aux.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   absh_r a * (i + 1) + absh_b1 a ==
                   absh_r a * i + absh_b1 a + absh_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 (absh_r a * S i + absh_b1 a))
                   (fl (absh_r a * i + absh_b1 a) + 1%nat)); auto.
                 rewrite <- fl_plus_int_rewrite.
                 apply fl_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   absh_r a * (i + 1) + absh_b1 a ==
                   absh_r a * i + absh_b1 a + absh_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 (absh_r a * S i + absh_b1 a))
                   (fl (absh_r a * i + absh_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: absh_r a * S i == S i * absh_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 (absh_r a * S i + absh_b1 a))
                 (absh_r a * S i + absh_b1 a)
                 (ones_early_alt a i + 1%nat)%Z); auto.
             elim (fl_def (absh_r a * S i + absh_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: abstractionh,
    forall H_wf: well_formed_abstractionh 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 (absh_r a * O%nat + absh_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 (absh_r a * 0%nat + absh_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 (absh_r a * S i + absh_b0 a)))).
       intro H_tmp; destruct H_tmp.
       elim (Zmin_spec (S i) (cg (absh_r a * (S i) + absh_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 (absh_r a * S i + absh_b0 a))
                 (cg (absh_r a * i + absh_b0 a))); auto.
             apply Zle_ge.
             apply cg_monotone_linear.
             assert (H_aux:
               absh_r a * i + absh_b0 a ==
               absh_r a * i + absh_b0 a + 0).
               ring.
             rewrite H_aux; clear H_aux.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               absh_r a * (i + 1) + absh_b0 a ==
               absh_r a * i + absh_b0 a + absh_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 (absh_r a * S i + absh_b0 a))
               (cg (absh_r a * i + absh_b0 a))); auto.
             apply cg_monotone_linear.
             assert (H_aux:
               absh_r a * i + absh_b0 a ==
               absh_r a * i + absh_b0 a + 0).
               ring.
             rewrite H_aux; clear H_aux.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               absh_r a * (i + 1) + absh_b0 a ==
               absh_r a * i + absh_b0 a + absh_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: absh_r a * S i + absh_b0 a <= ones_late a i).
           clear H0; clear H2.
           rewrite H_cc_aux1.
           apply (Qle_trans
             (absh_r a * S i + absh_b0 a)
             (cg(absh_r a * S i + absh_b0 a))
             0).
           destruct (cg_def_linear (absh_r a * S i + absh_b0 a)); assumption.
           apply Zle_impl_Qle.
           apply Zge_le.
           assumption.

         rewrite red_ones_late.
         case_eq (absh_r a * S i + absh_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 < absh_r a * S i + absh_b0 a); auto.
         apply Qle_not_lt.
         assumption.

       intro H_tmp; destruct H_tmp.
       elim (Zmin_spec (S i) (cg (absh_r a * (S i) + absh_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 (absh_r a * i + absh_b0 a) + 1)).
             apply inj_lt.
             auto with arith.
             rewrite <- cg_plus_int_rewrite.
             apply (Zle_trans
               (S i)
               (cg (absh_r a * S i + absh_b0 a))
               (cg (absh_r a * i + absh_b0 a + 1))); auto.
             apply cg_monotone_linear.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               absh_r a * (i + 1) + absh_b0 a ==
               absh_r a * i + absh_b0 a + absh_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: absh_r a * S i + absh_b0 a > ones_late a i).
           rewrite H_cc_aux1.
           apply (Qle_lt_trans
             i
             (cg (absh_r a * S i + absh_b0 a) - 1)%Z
             (absh_r a * S i + absh_b0 a));
           try solve [ elim (cg_def_linear (absh_r a * S i + absh_b0 a));
                       intros; assumption ].
           assert (H_aux:
             (cg (absh_r a * S i + absh_b0 a) - 1%nat) ==
             (cg (absh_r a * S i + absh_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 (absh_r a * S i + absh_b0 a) + - (1) + - i ==
             cg (absh_r a * S i + absh_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: absh_r a * S i + absh_b0 a > ones_late a i).
             rewrite Qlt_alt.
             case_eq (absh_r a * S i + absh_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)
                 (absh_r a * S i + absh_b0 a)
                 (cg (absh_r a * S i + absh_b0 a))); auto.
             elim (cg_def_linear (absh_r a * S i + absh_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:
                   absh_r a * (i + 1) + absh_b0 a ==
                   absh_r a * i + absh_b0 a + absh_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 (absh_r a * S i + absh_b0 a))
                     (cg (absh_r a * i + absh_b0 a) + 1%nat)); auto.
                 rewrite <- cg_plus_int_rewrite.
                 apply cg_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   absh_r a * (i + 1) + absh_b0 a ==
                   absh_r a * i + absh_b0 a + absh_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 (absh_r a * S i + absh_b0 a))
                   (cg (absh_r a * i + absh_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: absh_r a * S i == S i * absh_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: absh_r a * S i + absh_b0 a <= ones_late a i).
             rewrite Qge_alt.
             case_eq (absh_r a * S i + absh_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 < absh_r a * S i + absh_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:
                   absh_r a * i + absh_b0 a ==
                   absh_r a * i + absh_b0 a + 0).
                   ring.
                 rewrite H_aux; clear H_aux.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   absh_r a * (i + 1) + absh_b0 a ==
                   absh_r a * i + absh_b0 a + absh_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 (absh_r a * S i + absh_b0 a))
                     (cg (absh_r a * i + absh_b0 a) + 1%nat)); auto.
                 rewrite <- cg_plus_int_rewrite.
                 apply cg_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   absh_r a * (i + 1) + absh_b0 a ==
                   absh_r a * i + absh_b0 a + absh_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 (absh_r a * S i + absh_b0 a))
                   (cg (absh_r a * i + absh_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: absh_r a * S i == S i * absh_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) <= (absh_r a * S i + absh_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) ?= absh_r a * S i + absh_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) > (absh_r a * S i + absh_b1 a).
  Proof.
    intros.
    simpl in H_w.
    case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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: abstractionh,
    forall H_wf_a: well_formed_abstractionh a,
    forall H_w_in_a: in_abstractionh 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 ?= absh_r a * 1%nat + absh_b1 a);
          try solve [ intros; apply le_refl ].
        intros H_cmp.
        rewrite <- Qgt_alt in H_cmp.
        absurd (absh_r a * 1 + absh_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 ?= absh_r a * 1%nat + absh_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')) ?= absh_r a * S (S i') + absh_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')) ?= absh_r a * S (S i') + absh_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')) ?= absh_r a * S (S i') + absh_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')) ?= absh_r a * S (S i') + absh_b1 a);
              try omega.
            intro H_cmp'.
            rewrite <- Qgt_alt in H_cmp'.
            absurd (absh_r a * S (S i') + absh_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')) ?= absh_r a * S (S i') + absh_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')) ?= absh_r a * S (S i') + absh_b1 a);
        omega.
  Qed.

  Property ones_late_le_ones_w:
    forall w: ibw,
    forall a: abstractionh,
    forall H_wf_a: well_formed_abstractionh a,
    forall H_w_in_a: in_abstractionh 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 (absh_r a * 1%nat + absh_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 (absh_r a * 1%nat + absh_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 < absh_r a * 1 + absh_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 (absh_r a * S (S i') + absh_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 (absh_r a * S (S i') + absh_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'))
            (absh_r a * S (S i') + absh_b0 a)
            (ones w (S i')));
          try solve [ exact H_cmp ].
        unfold in_abstractionh 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: abstractionh,
   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) ?= absh_r a * S i + absh_b1 a);
        try reflexivity.
        intro H_cmp.
        case_eq (absh_r a * S i + absh_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: abstractionh,
   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 (absh_r a * S i + absh_b0 a ?= ones_late a i);
        try reflexivity.
        intro H_cmp.
        case_eq (S (ones_late a i) ?= absh_r a * S i + absh_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: abstractionh,
    forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
    forall H_absh_b1_lt_absh_b0: absh_b1 a - absh_b0 a < 1,
    forall i,
    ones_late a i = ones_early a i.
  Proof.
    induction i.
      simpl.
      reflexivity.

      simpl.
      case_eq (absh_r a * S i + absh_b0 a ?= ones_late a i).
        intros H_cmp_zero.
        rewrite IHi.
        case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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 (absh_r a * S i + absh_b1 a == absh_r a * S i + absh_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:
            absh_b0 a + 1 + - absh_b1 a == 1 + - (absh_b1 a - absh_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) < absh_r a * S i + absh_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:
            absh_b0 a + 1 + - absh_b1 a == 1 + - (absh_b1 a - absh_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) ?= absh_r a * S i + absh_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 == absh_r a * S i + absh_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 (absh_r a * S i + absh_b0 a < absh_r a * S i + absh_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:
            absh_b0 a + - (absh_b1 a + - (1)) == 1 + - (absh_b1 a - absh_b0 a)).
            ring.
          rewrite H_aux; clear H_aux.
          apply -> Qlt_minus_iff.
          assumption.

          intros H_cmp_one.
          rewrite <- Qlt_alt in *.
          absurd (absh_r a * S i + absh_b0 a < absh_r a * S i + absh_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:
              absh_b0 a + - (absh_b1 a + - (1)) == 1 + - (absh_b1 a - absh_b0 a)).
              ring.
            rewrite H_aux; clear H_aux.
            apply -> Qlt_minus_iff.
            assumption.

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

          reflexivity.

        intros H_cmp_zero.
        rewrite IHi.
        case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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: abstractionh,
    forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
    in_abstractionh (w_early a) a.
  Proof.
    intros.
    unfold in_abstractionh.
    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: (absh_r a * S i' + absh_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 (absh_r a * S i' + absh_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
              (absh_r a * S i' + absh_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 (absh_b1 a - absh_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
                  (absh_r a * S (S i'') + absh_b0 a)
                  (absh_r a * S (S i'') + (absh_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:
                  absh_b1 a - 1 + - absh_b0 a == absh_b1 a - absh_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'') + - (absh_r a * S (S i'') + (absh_b1 a - 1)) ==
                  ones_early a (S i'') + 1 + - (absh_r a * S (S i'') + absh_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: abstractionh,
    forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
    in_abstractionh (w_late a) a.
  Proof.
    intros.
    unfold in_abstractionh.
    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 (absh_r a * S i' + absh_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') ?= absh_r a * S i' + absh_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'))
                (absh_r a * S i' + absh_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 (absh_b1 a - absh_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'))
                (absh_r a * S i' + absh_b0 a + 1)
                (absh_r a * S i' + absh_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:
                  absh_b1 a + - (absh_b0 a + 1) == absh_b1 a - absh_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 (absh_r a * S i' + absh_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: abstractionh,
    forall H_wf: well_formed_abstractionh 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: abstractionh,
    forall H_wf: well_formed_abstractionh a,
    forall H_non_empty: non_empty a,
    in_abstractionh (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: abstractionh,
    forall H_wf: well_formed_abstractionh a,
    forall H_non_empty: non_empty a,
    in_abstractionh (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_abstractionh a1,
    forall H_wf_a2: well_formed_abstractionh a2,
    absh_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_abstractionh a1,
    forall H_wf_a2: well_formed_abstractionh a2,
    absh_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.

End early_and_late_properties.

Lemma ones_late_le_ones_early_impl_non_empty:
  forall a,
  forall H_wf: well_formed_abstractionh 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_abstractionh 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 (absh_r a * i + absh_b1 a) =
       fl (Qred (absh_r a * i + absh_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
        (absh_r a * i + absh_b0 a)
        (absh_r a * i + (absh_b1 a - (1 - (1 # Qden (Qred (absh_r a * i + absh_b1 a))))))
        (Qred (absh_r a * i + absh_b1 a) - (1 - (1 # Qden (Qred (absh_r a * i + absh_b1 a)))))).
      apply Qplus_le_compat; try solve [ apply Qle_refl ].
      apply
        (Qle_trans
          (absh_b0 a)
          (absh_b1 a - (1 - (1 # Qden (absh_r a))))
          (absh_b1 a - (1 - (1 # Qden (Qred (absh_r a * i + absh_b1 a)))))).
        apply <- Qle_minus_iff.
        assert (H_aux:
          absh_b1 a - (1 - (1 # Qden (absh_r a))) + - absh_b0 a ==
          absh_b1 a - absh_b0 a + - (1 - (1 # Qden (absh_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: abstractionh,
    forall H_a1_eq_a2: absh_equal a1 a2,
    forall H_non_empty1: non_empty_test a1,
    forall H_den:
      1 # Qden (absh_b1 a1) * Qden (absh_r a1) <=
      1 # Qden (absh_b1 a2) * Qden (absh_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 (absh_b1 a2) * Qden (absh_r a2)))
        (1 - (1 # Qden (absh_b1 a1) * Qden (absh_r a1)))
        (absh_b1 a2 - absh_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: abstractionh,
    absh_equal a (absh_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_abstractionh 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 := absh_std a).
    assert (H_a_eq_a_std: absh_equal a a_std).
      apply abs_equal_abs_std_non_empty.
    assert (H_wf_std: well_formed_abstractionh a_std).
      apply (well_formed_abstractionh_absh_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.

  Lemma on_w1_w2_le_on_a1_a2:
    forall (w1:ibw) (w2:ibw),
    forall (a1:abstractionh) (a2:abstractionh),
    forall H_wf_a1: well_formed_abstractionh a1,
    forall H_wf_a2: well_formed_abstractionh a2,
    forall (H_a1_eq_absh_w1: in_abstractionh w1 a1),
    forall (H_a2_eq_absh_w2: in_abstractionh 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 <=
    (absh_r a1 * absh_r a2) * i + (absh_b1 a1 * absh_r a2 + absh_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 <= absh_r a1 * i + absh_b1 a1).
      unfold in_abstractionh in H_a1_eq_absh_w1.
      generalize (H_a1_eq_absh_w1 i H_i_ge_1).
      clear H_a1_eq_absh_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) <= (absh_r a2 * ones w1 i + absh_b1 a2)).
      unfold in_abstractionh in H_a2_eq_absh_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_absh_w2 (ones w1 i) H_ones_w1_ge_1).
      clear H_a2_eq_absh_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))
        (absh_r a2 * ones w1 i + absh_b1 a2)
        (absh_r a1 * absh_r a2 * i + (absh_b1 a1 * absh_r a2 + absh_b1 a2))
        H_w2_le_a2).
    assert (H_aux:
      absh_r a1 * absh_r a2 * i + (absh_b1 a1 * absh_r a2 + absh_b1 a2) ==
      (absh_r a1 * absh_r a2 * i + absh_b1 a1 * absh_r a2) + absh_b1 a2).
      ring.
    rewrite H_aux; clear H_aux.
    apply Qplus_le_compat; try solve [ apply Qle_refl ].
    assert (H_aux:
      absh_r a1 * absh_r a2 * i + absh_b1 a1 * absh_r a2 ==
      (absh_r a1 * i + absh_b1 a1) * absh_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 absh_b0_neg_impl_ones_ge_a:
    forall (w:ibw) (a:abstractionh),
    forall H_wf_a: well_formed_abstractionh a,
    forall H_flo: absh_b0 a <= 0,
    forall H_a_eq_absh_w: in_abstractionh w a,
    forall i:nat,
    ones w i >= absh_r a * i + absh_b0 a.
  Proof.
    induction i.
      assert (H_aux: absh_r a * 0 == 0).
        ring.
      rewrite H_aux; clear H_aux.
      assert (H_aux: 0 + absh_b0 a == absh_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:
          absh_r a * (i + 1) + absh_b0 a ==
          absh_r a * i + absh_b0 a + absh_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_abstractionh in H_a_eq_absh_w.
        assert (H_S_i_ge_1:(S i >= 1)%nat).
          auto with arith.
        generalize (H_a_eq_absh_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
            (absh_r a * S i + absh_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:abstractionh) (a2:abstractionh),
    forall H_wf_a1: well_formed_abstractionh a1,
    forall H_flo_a1: absh_b0 a1 <= 0,
    forall H_wf_a2: well_formed_abstractionh a2,
    forall H_flo_a2: absh_b0 a2 <= 0,
    forall (H_a1_eq_absh_w1: in_abstractionh w1 a1),
    forall (H_a2_eq_absh_w2: in_abstractionh w2 a2),
    forall i,
    forall (H_on: on w1 w2 i = false),
     absh_r a1 * absh_r a2 * i + (absh_b0 a1 * absh_r a2 + absh_b0 a2)
     <= ones (on w1 w2) i.
  Proof.
    intros.
    rewrite ones_on_def.
    generalize (absh_b0_neg_impl_ones_ge_a H_wf_a1 H_flo_a1 H_a1_eq_absh_w1 i).
    intro H_w1_ge_a1.
    generalize (absh_b0_neg_impl_ones_ge_a H_wf_a2 H_flo_a2 H_a2_eq_absh_w2 (ones w1 i)).
    intro H_w2_ge_a2.
    apply
      (Qle_trans
        (absh_r a1 * absh_r a2 * i + (absh_b0 a1 * absh_r a2 + absh_b0 a2))
        (absh_r a2 * ones w1 i + absh_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 <= absh_r a2)).
      apply H_wf_a2.
    generalize
      (Qmult_le_compat_r
        (absh_r a1 * i + absh_b0 a1)
        (ones w1 i)
        (absh_r a2)
        H_w1_ge_a1
        (H_r_pos_2)).
    intro H_cc.
    rewrite Qmult_plus_distr_l in H_cc.
    assert (H_aux: absh_r a1 * i * absh_r a2 == absh_r a1 * absh_r a2 * i).
      ring.
    rewrite H_aux in H_cc; clear H_aux.
    assert (H_aux: ones w1 i * absh_r a2 == absh_r a2 * ones w1 i).
      ring.
    rewrite H_aux in H_cc; clear H_aux.
    exact H_cc.
  Qed.

  Property on_absh_correctness_aux:
    forall (w1:ibw) (w2:ibw),
    forall (a1:abstractionh) (a2:abstractionh),
    forall H_wf_a1: well_formed_abstractionh a1,
    forall H_wf_a2: well_formed_abstractionh a2,
    forall (H_a1_eq_absh_w1: in_abstractionh w1 a1),
    forall (H_a2_eq_absh_w2: in_abstractionh w2 a2),
    in_abstractionh (on w1 w2) (on_absh a1 a2).
  Proof.
    intros.

    assert (H_aux:
      exists a1_0,
        (absh_b1 a1_0 == absh_b1 a1) /\
        (absh_b0 a1_0 == 0) /\
        (absh_r a1_0 == absh_r a1)).
      exists (abshmake (absh_b1 a1) 0 (absh_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_abstractionh a1_0).
      unfold well_formed_abstractionh.
      destruct H_a1_0.
      destruct H0.
      rewrite H1.
      assumption.
    assert (H_absh_b01_0: absh_b0 a1_0 <= 0).
      destruct H_a1_0.
      destruct H0.
      rewrite H0.
      eapply Qle_refl.

    assert (H_aux:
      exists a2_0,
        (absh_b1 a2_0 == absh_b1 a2) /\
        (absh_b0 a2_0 == 0) /\
        (absh_r a2_0 == absh_r a2)).
      exists (abshmake (absh_b1 a2) 0 (absh_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_abstractionh a2_0).
      unfold well_formed_abstractionh.
      destruct H_a2_0.
      destruct H0.
      rewrite H1.
      assumption.
    assert (H_absh_b02_0: absh_b0 a2_0 <= 0).
      destruct H_a2_0.
      destruct H0.
      rewrite H0.
      eapply Qle_refl.

    unfold in_abstractionh.
    intros.

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

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

        clear H_aux1 H_aux2.
        intros H_absh_b01 H_absh_b02.
        elim (Qlt_alt (absh_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b01).
        clear H_aux1 H_aux2.
        intro H_absh_b01_eq_cmp.
        elim (Qlt_alt (absh_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b02).
        clear H_aux1 H_aux2.
        intro H_absh_b02_eq_cmp.
        simpl.
        rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.
        apply
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 (Qlt_le_weak (absh_b0 a1) 0 H_absh_b01)
            H_wf_a2 (Qlt_le_weak (absh_b0 a2) 0 H_absh_b02)
            H_a1_eq_absh_w1 H_a2_eq_absh_w2);
          auto.

        clear H_aux1 H_aux2.
        intros H_absh_b01 H_absh_b02.
        elim (Qgt_alt (absh_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b01).
        clear H_aux1 H_aux2.
        intro H_absh_b01_eq_cmp.
        elim (Qlt_alt (absh_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b02).
        clear H_aux1 H_aux2.
        intro H_absh_b02_eq_cmp.
        simpl.
        rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.

        assert (H_a1_0_eq_absh_w1: in_abstractionh w1 a1_0).
          assert (H_a1_in_a1_0: absh_included_test a1 a1_0).
            apply absh_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_absh_w1).

        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1_0 H_absh_b01_0
            H_wf_a2 (Qlt_le_weak (absh_b0 a2) 0 H_absh_b02)
            H_a1_0_eq_absh_w1 H_a2_eq_absh_w2
            i H_on).
        decompose [and] H_a1_0.
        rewrite H2, H1.
        trivial.

        clear H_aux1 H_aux2.
        intros H_absh_b01 H_absh_b02.
        elim (Qlt_alt (absh_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b01).
        clear H_aux1 H_aux2.
        intro H_absh_b01_eq_cmp.
        elim (Qgt_alt (absh_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b02).
        clear H_aux1 H_aux2.
        intro H_absh_b02_eq_cmp.
        simpl.
        rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.

        assert (H_a2_0_eq_absh_w2: in_abstractionh w2 a2_0).
          assert (H_a2_in_a2_0: absh_included_test a2 a2_0).
            apply absh_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_absh_w2).

        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 (Qlt_le_weak (absh_b0 a1) 0 H_absh_b01)
            H_wf_a2_0 H_absh_b02_0
            H_a1_eq_absh_w1 H_a2_0_eq_absh_w2
            i H_on).
        decompose [and] H_a2_0.
        rewrite H2, H1.
        trivial.

        clear H_aux1 H_aux2.
        intros H_absh_b01 H_absh_b02.
        elim (Qgt_alt (absh_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b01).
        clear H_aux1 H_aux2.
        intro H_absh_b01_eq_cmp.
        elim (Qgt_alt (absh_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b02).
        clear H_aux1 H_aux2.
        intro H_absh_b02_eq_cmp.
        simpl.
        rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.

        assert (H_a1_0_eq_absh_w1: in_abstractionh w1 a1_0).
          assert (H_a1_in_a1_0: absh_included_test a1 a1_0).
            apply absh_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_absh_w1).

        assert (H_a2_0_eq_absh_w2: in_abstractionh w2 a2_0).
          assert (H_a2_in_a2_0: absh_included_test a2 a2_0).
            apply absh_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_absh_w2).

        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1_0 H_absh_b01_0
            H_wf_a2_0 H_absh_b02_0
            H_a1_0_eq_absh_w1 H_a2_0_eq_absh_w2
            i H_on).
        decompose [and] H_a1_0.
        rewrite H2, H1.
        decompose [and] H_a2_0.
        rewrite H5, H4.
        trivial.

        intros H_absh_b02 H_aux.
        elim H_aux.
        clear H_aux.
        intro H_absh_b01.
        elim (Qlt_alt (absh_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b01).
        clear H_aux1 H_aux2.
        intro H_absh_b01_eq_cmp.
        elim (Qeq_alt (absh_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b02).
        clear H_aux1 H_aux2.
        intro H_absh_b02_eq_cmp.
        simpl.
        rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.
        assert (H_absh_b02_le_0: absh_b0 a2 <= 0).
          rewrite H_absh_b02.
          apply Qle_refl.
        apply
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 (Qlt_le_weak (absh_b0 a1) 0 H_absh_b01)
            H_wf_a2 H_absh_b02_le_0
            H_a1_eq_absh_w1 H_a2_eq_absh_w2);
          auto.

        clear H_aux.
        intro H_absh_b01.
        elim (Qgt_alt (absh_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b01).
        clear H_aux1 H_aux2.
        intro H_absh_b01_eq_cmp.
        elim (Qeq_alt (absh_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b02).
        clear H_aux1 H_aux2.
        intro H_absh_b02_eq_cmp.
        simpl.
        rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.

        assert (H_a1_0_eq_absh_w1: in_abstractionh w1 a1_0).
          assert (H_a1_in_a1_0: absh_included_test a1 a1_0).
            apply absh_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_absh_w1).

        assert (H_absh_b02_le_0: absh_b0 a2 <= 0).
          rewrite H_absh_b02.
          apply Qle_refl.
        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1_0 H_absh_b01_0
            H_wf_a2 H_absh_b02_le_0
            H_a1_0_eq_absh_w1 H_a2_eq_absh_w2
            i H_on).
        decompose [and] H_a1_0.
        rewrite H2, H1.
        trivial.

        intros H_aux H_absh_b01.
        elim H_aux.
        clear H_aux.
        intro H_absh_b02.
        elim (Qeq_alt (absh_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b01).
        clear H_aux1 H_aux2.
        intro H_absh_b01_eq_cmp.
        elim (Qlt_alt (absh_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b02).
        clear H_aux1 H_aux2.
        intro H_absh_b02_eq_cmp.
        simpl.
        rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.
        assert (H_absh_b01_le_0: absh_b0 a1 <= 0).
          rewrite H_absh_b01.
          apply Qle_refl.
        apply
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 H_absh_b01_le_0
            H_wf_a2 (Qlt_le_weak (absh_b0 a2) 0 H_absh_b02)
            H_a1_eq_absh_w1 H_a2_eq_absh_w2);
          auto.

        clear H_aux.
        intro H_absh_b02.
        elim (Qeq_alt (absh_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b01).
        clear H_aux1 H_aux2.
        intro H_absh_b01_eq_cmp.
        elim (Qgt_alt (absh_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b02).
        clear H_aux1 H_aux2.
        intro H_absh_b02_eq_cmp.
        simpl.
        rewrite H_absh_b01_eq_cmp.
        rewrite H_absh_b02_eq_cmp.

        assert (H_a2_0_eq_absh_w2: in_abstractionh w2 a2_0).
          assert (H_a2_in_a2_0: absh_included_test a2 a2_0).
            apply absh_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_absh_w2).

        assert (H_absh_b01_le_0: absh_b0 a1 <= 0).
          rewrite H_absh_b01.
          apply Qle_refl.
        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 H_absh_b01_le_0
            H_wf_a2_0 H_absh_b02_0
            H_a1_eq_absh_w1 H_a2_0_eq_absh_w2
            i H_on).
        decompose [and] H_a2_0.
        rewrite H2, H1.
        trivial.

        intros H_absh_b02 H_absh_b01.
        elim (Qeq_alt (absh_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b01).
        clear H_aux1 H_aux2.
        intro H_absh_b01_eq_cmp.
        elim (Qeq_alt (absh_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absh_b02).
        clear H_aux1 H_aux2.
        intro H_absh_b02_eq_cmp.
        simpl.
        rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.

        assert (H_absh_b01_le_0: absh_b0 a1 <= 0).
          rewrite H_absh_b01.
          apply Qle_refl.
        assert (H_absh_b02_le_0: absh_b0 a2 <= 0).
          rewrite H_absh_b02.
          apply Qle_refl.
        apply
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 H_absh_b01_le_0
            H_wf_a2 H_absh_b02_le_0
            H_a1_eq_absh_w1 H_a2_eq_absh_w2
            i H_on).
  Qed.

End on_properties.


Section not_properties.

  Property not_absh_correctness_aux:
    forall w: ibw,
    forall a:abstractionh,
    forall H_wf_a: well_formed_abstractionh a,
    forall H_a_eq_absh_w: in_abstractionh w a,
    in_abstractionh (not w) (not_absh a).
  Proof.
    intros.
    unfold in_abstractionh.
    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_absh_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 - absh_r a) * 1 + - absh_b0 a + - (1) ==
            0 + - (absh_r a * 1 + absh_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_absh_w 1%nat H_i_ge_1).
          clear H_a_eq_absh_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_absh_b1.

          rewrite H_w in *.
          simpl.
          simpl in H_absh_b1.
          apply <- Qle_minus_iff.
          assert (H_aux:
            0 + - ((1 - absh_r a) * 1 + - absh_b1 a) ==
            absh_r a * 1 + absh_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: absh_r a * S (S i') + absh_b0 a <= ones w (S (S i'))).
              unfold in_abstractionh in H_a_eq_absh_w.
              generalize (H_a_eq_absh_w (S (S i')) H_i_ge_1).
              clear H_a_eq_absh_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 - absh_r a) * (S i' + 1) + - absh_b0 a + - (i' - ones w i' + 1) ==
              ones w i' + (S i' - i') + - (absh_r a * (S i' + 1) + absh_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: absh_r a * S (S i') + absh_b0 a <= ones w (S (S i'))).
              unfold in_abstractionh in H_a_eq_absh_w.
              generalize (H_a_eq_absh_w (S (S i')) H_i_ge_1).
              clear H_a_eq_absh_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 - absh_r a) * S (S i') + - absh_b0 a + - (i' - ones w i' + 1 + 1) ==
              ones w i' + (S (S i') - i' - 1 - 1) + - (absh_r a * S (S i') + absh_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')) <= absh_r a * (S (S i')) + absh_b1 a).
              unfold in_abstractionh in H_a_eq_absh_w.
              generalize (H_a_eq_absh_w (S (S i')) H_i_ge_1).
              clear H_a_eq_absh_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 - absh_r a) * S (S i') + - absh_b1 a) ==
              absh_r a * S (S i') + absh_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_absh_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 - absh_r a) * 2 + - absh_b1 a) ==
                absh_r a * 2 + absh_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')) <= absh_r a * S (S i') + absh_b1 a).
                unfold in_abstractionh in H_a_eq_absh_w.
                generalize (H_a_eq_absh_w (S (S i')) H_i_ge_1).
                clear H_a_eq_absh_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.
              rewrite ones_S_i_eq_S_ones_i in H_ones_w_le_a; auto.
              simpl in H_ones_w_le_a.
              rewrite <- n_plus_1_eq_S_n in H_ones_w_le_a.
              rewrite <- n_plus_1_eq_S_n in H_ones_w_le_a.

              apply <- Qle_minus_iff.
              assert (H_aux:
                i' - ones w i' + - ((1 - absh_r a) * S (S i') + - absh_b1 a) ==
                absh_r a * S (S i') + absh_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_S_i'.
          assert (H_not_w_S_i': not w (S i') = true).
            unfold not.
            rewrite H_w_S_i'.
            simpl.
            trivial.
          rewrite ones_S_i_eq_ones_i; auto.
          simpl.
          rewrite H_w_S_i'.
          simpl.

          rewrite <- (n_plus_1_eq_S_n (ones (not w) i')).
          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')) <= absh_r a * S (S i') + absh_b1 a).
            unfold in_abstractionh in H_a_eq_absh_w.
            generalize (H_a_eq_absh_w (S (S i')) H_i_ge_1).
            clear H_a_eq_absh_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.
            rewrite ones_S_i_eq_ones_i in H_ones_w_le_a; auto.
            simpl in H_ones_w_le_a.
            rewrite <- n_plus_1_eq_S_n in H_ones_w_le_a.

            apply <- Qle_minus_iff.
            assert (H_aux:
              i' - ones w i' + 1 + - ((1 - absh_r a) * S (S i') + - absh_b1 a) ==
              absh_r a * S (S i') + absh_b1 a + - (ones w i' + S (S i') - i' - 1)).
              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' - 1 == ones w i' + 1).
              ring.
            rewrite H_aux; clear H_aux.
            assumption.
  Qed.

  Lemma absh_included_test_not_not_absh:
    forall a: abstractionh,
    absh_included_test a (not_absh (not_absh a)).
  Proof.
    intros.
    unfold absh_included_test.
    repeat split.
      simpl.
      ring.

      simpl.
      ring_simplify.
      apply Qle_refl.

      simpl.
      ring_simplify.
      apply Qle_refl.
  Qed.

  Lemma not_not_absh_included_test_absh:
    forall a: abstractionh,
    absh_included_test (not_absh (not_absh a)) a.
  Proof.
    intros.
    unfold absh_included_test.
    repeat split.
      simpl.
      ring.

      simpl.
      ring_simplify.
      apply Qle_refl.

      simpl.
      ring_simplify.
      apply Qle_refl.
  Qed.

  Property not_not_absh_equal_absh:
    forall a: abstractionh,
    absh_equal (not_absh (not_absh a)) a.
  Proof.
    intros.
    apply absh_equiv_test_impl_absh_equal.
    split.
      apply not_not_absh_included_test_absh.
      apply absh_included_test_not_not_absh.
  Qed.

  Property not_absh_well_formed_abstractionh_compat:
    forall a: abstractionh,
    forall H_wf: well_formed_abstractionh a,
    well_formed_abstractionh (not_absh a).
  Proof.
    intros.
    unfold well_formed_abstractionh.
    simpl.
    destruct H_wf as [H0 H1].
    split.
      apply -> Qle_minus_iff.
      assumption.

      apply <- Qle_minus_iff.
      ring_simplify.
      assumption.
  Qed.

End not_properties.


Section prec_absh_properties.

  Property w_early_prec_a:
    forall a: abstractionh,
    forall H_wf: well_formed_abstractionh a,
    forall w: ibw,
    forall H_w_in_a: in_abstractionh w a,
    prec (w_early a) w.
  Proof.
    intros.
    unfold prec.
    unfold ge.
    intros.
    rewrite <- ones_early_eq_ones_w_early.
    apply ones_w_le_ones_early; assumption.
  Qed.

  Property a_prec_w_late:
    forall a: abstractionh,
    forall H_wf: well_formed_abstractionh a,
    forall w: ibw,
    forall H_w_in_a: in_abstractionh w a,
    prec w (w_late a).
  Proof.
    intros.
    unfold prec.
    unfold ge.
    intros.
    rewrite <- ones_late_eq_ones_w_late.
    apply ones_late_le_ones_w; assumption.
  Qed.

  Property prec_absh_alt_correctness:
    forall a1 a2: abstractionh,
    forall H_wf1: well_formed_abstractionh a1,
    forall H_wf2: well_formed_abstractionh a2,
    forall H_prec_test: prec_absh_alt a1 a2,
    prec_absh a1 a2.
  Proof.
    intros.
    unfold prec_absh.
    intros.
    pose (H_early2_prec_w2:= w_early_prec_a H_wf2 H_w2_in_a2).
    unfold prec_absh_alt in H_prec_test.
    pose (H_w1_prec_late1:= a_prec_w_late H_wf1 H_w1_in_a1).
    assert (H_w1_prec_w_early2: prec w1 (w_early a2)).
      apply (prec_trans H_w1_prec_late1 H_prec_test).
    apply (prec_trans H_w1_prec_w_early2 H_early2_prec_w2).
  Qed.

  Property prec_absh_alt_complet:
    forall a1 a2: abstractionh,
    forall H_wf1: well_formed_abstractionh a1,
    forall H_non_empty1: non_empty a1,
    forall H_wf2: well_formed_abstractionh a2,
    forall H_non_empty2: non_empty a2,
    forall H_prec: prec_absh a1 a2,
    prec_absh_alt a1 a2.
  Proof.
    intros.
    unfold prec_absh_alt.
    unfold prec_absh in H_prec.
    apply H_prec.
    apply late_in_abs; auto.
    apply early_in_abs; auto.
  Qed.

  Property prec_absh_test_correctness_aux:
    forall a1 a2: abstractionh,
    forall H_wf1: well_formed_abstractionh a1,
    forall H_wf2: well_formed_abstractionh a2,
    forall H_prec_test: prec_absh_test a1 a2,
    forall H_sync: absh_r a1 == absh_r a2,
    prec_absh a1 a2.
  Proof.
    intros.
    apply prec_absh_alt_correctness; auto.
    unfold prec_absh_alt.
    unfold prec.
    intro i.
    rewrite <- ones_early_eq_ones_w_early.
    rewrite <- ones_late_eq_ones_w_late.
    unfold ge.
    apply inj_le_rev.
    rewrite ones_early_eq_ones_early_alt; auto.
    rewrite ones_late_eq_ones_late_alt; auto.
    rewrite ones_early_alt_remove_Zabs_nat.
    rewrite ones_late_alt_remove_Zabs_nat.
    apply Zmax_le_compat_l.
    apply Zmin_le_compat_l.
    apply Zlt_impl_Zle.

    rewrite <- cg_plus_int_rewrite.
    apply x_lt_y_impl_fl_x_lt_cg_y; auto.
    rewrite H_sync.
    rewrite <- Qplus_assoc.
    apply Qplus_lt_compat_l.
    unfold prec_absh_test in H_prec_test.
    apply <- Qlt_minus_iff.
    assert (H_aux:
      absh_b0 a1 + 1 + - absh_b1 a2 == 1 + - (absh_b1 a2 - absh_b0 a1)).
      ring.
    rewrite H_aux; clear H_aux.
    apply -> Qlt_minus_iff.
    assumption.
  Qed.

End prec_absh_properties.

Section subtyping_properties.

  Property subtyping_absh_impl_subtyping_absh_alt:
    forall a1 a2: abstractionh,
    forall H_sub: subtyping_absh a1 a2,
    subtyping_absh_alt a1 a2.
  Proof.
    intros.
    unfold subtyping_absh_alt.
    unfold subtyping_absh in H_sub.
    split.
      unfold prec_absh.
      intros.
      unfold subtyping in H_sub.
      destruct (H_sub w1 w2 H_w1_in_a1 H_w2_in_a2).
      assumption.

      unfold sync_absh.
      intros.
      unfold subtyping in H_sub.
      destruct (H_sub w1 w2 H_w1_in_a1 H_w2_in_a2).
      assumption.
  Qed.

  Property subtyping_absh_alt_impl_subtyping_absh:
    forall a1 a2: abstractionh,
    forall H_sub: subtyping_absh_alt a1 a2,
    subtyping_absh a1 a2.
  Proof.
    intros.
    unfold subtyping_absh.
    unfold subtyping_absh_alt in H_sub.
    elim H_sub; intros H_prec H_sync.
    intros.
    split.
      apply H_prec; auto.

      apply H_sync; auto.
  Qed.

End subtyping_properties.