Library abstraction_jfla_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_jfla_def.

Section Abstractionj_def.

  Definition absj_equal (a1: abstractionj) (a2:abstractionj) :=
    (absj_r a1 == absj_r a2) /\
    (absj_b1 a1) == (absj_b1 a2) /\
    (absj_b0 a1) == (absj_b0 a2).

  Instance absj_equal_is_equiv : Equivalence _ absj_equal.
  Proof.
    constructor ; unfold absj_equal ; red ; intuition.
    transitivity (absj_r y) ; auto.
    transitivity (absj_b1 y) ; auto.
    transitivity (absj_b0 y) ; auto.
  Qed.

End Abstractionj_def.

Definition absj_equiv (a1: abstractionj) (a2:abstractionj) :=
  absj_included a1 a2 /\ absj_included a2 a1.

Definition absj_equiv_test (a1: abstractionj) (a2:abstractionj) :=
  absj_included_test a1 a2 /\ absj_included_test a2 a1.

Section abstraction_equivalence_properties.

  Property absj_included_test_impl_absj_included:
    forall a1 a2: abstractionj,
    forall H_a1_in_test_a2: absj_included_test a1 a2,
    absj_included a1 a2.
  Proof.
    intros.
    unfold absj_included.
    intros.
    unfold in_abstractionj.
    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
          (Qlt_le_trans
            (ones w (pred i))
            (absj_r a1 * i + absj_b1 a1)
            (absj_r a1 * i + absj_b1 a2)); auto.
        apply Qplus_le_compat; auto.
        apply Qle_refl.

        intro H_w.
        apply
          (Qle_trans
            (absj_r a1 * i + absj_b0 a2)
            (absj_r a1 * i + absj_b0 a1)
            (ones w (pred 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_abstractionj a1,
    forall H_wf_a2: well_formed_abstractionj a2,
    forall H_a1_in_a2: absj_included_test a1 a2,
    forall H_w_in_a1: in_abstractionj w a1,
    in_abstractionj w a2.
  Proof.
    intros.
    unfold in_abstractionj.
    intros i H_i_ge_1.
    split.
      intro H_w.
      unfold in_abstractionj 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 (Qlt_le_trans
        (ones w (pred i))
        (absj_r a1 * i + absj_b1 a1)
        (absj_r a1 * i + absj_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_abstractionj 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.
      rewrite ones_pred_i_eq_ones_i in *; auto.
      apply
        (Qle_trans
          (absj_r a1 * i + absj_b0 a2)
          (absj_r a1 * i + absj_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 absj_weakening_aux:
    forall a1 a2: abstractionj,
    forall H_one: absj_b1 a1 <= absj_b1 a2,
    forall H_absj_b0: absj_b0 a1 >= absj_b0 a2,
    forall H_r: absj_r a1 == absj_r a2,
    absj_included_test a1 a2.
  Proof.
    intros.
    unfold absj_included_test.
    repeat split; auto.
  Qed.

  Property absj_weakening_0:
    forall a1 a2: abstractionj,
    forall H_absj_b01: absj_b0 a1 > 0,
    forall H_r: absj_r a1 == absj_r a2,
    forall H_one: absj_b1 a1 == absj_b1 a2,
    forall H_absj_b02: absj_b0 a2 == 0,
    absj_included_test a1 a2.
  Proof.
    intros.
    eapply absj_weakening_aux; auto.
    rewrite H_one.
    apply Qle_refl.
    rewrite H_absj_b02.
    eapply Qlt_le_weak.
    assumption.
  Qed.

  Property absj_equal_sym:
    forall a1 a2: abstractionj,
    forall H_a1_eq_a2: absj_equal a1 a2,
    absj_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 absj_equal_impl_absj_included_test:
    forall a1 a2: abstractionj,
    forall H_a1_eq_a2: absj_equal a1 a2,
    absj_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 absj_equal_impl_absj_equiv_test:
    forall a1 a2: abstractionj,
    forall H_a1_eq_a2: absj_equal a1 a2,
    absj_equiv_test a1 a2.
  Proof.
    intros.
    split.
      apply absj_equal_impl_absj_included_test; auto.
      apply absj_equal_impl_absj_included_test; auto.
      apply absj_equal_sym.
      assumption.
  Qed.

  Property absj_equiv_test_impl_absj_equal:
    forall a1 a2: abstractionj,
    forall H_a1_eq_a2: absj_equiv_test a1 a2,
    absj_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_absj_b11_le_absj_b12 H_absj_b02_le_absj_b01.
    elim H_tmp2; clear H_tmp2.
    intros H_r' H_tmp'.
    elim H_tmp'; clear H_tmp' H_r'.
    intros H_absj_b12_le_absj_b11 H_absj_b01_le_absj_b02.
    repeat split.
      trivial.
      apply Qle_antisym; assumption.
      apply Qle_antisym; assumption.
  Qed.

  Property absj_equal_correctness:
    forall a1 a2: abstractionj,
    forall H_wf1: well_formed_abstractionj a1,
    forall H_wf2: well_formed_abstractionj a2,
    forall w: ibw,
    forall H_w_in_a1: in_abstractionj w a1,
    forall H_eq: absj_equal a1 a2,
    in_abstractionj w a2.
  Proof.
    intros.
    apply absj_equal_impl_absj_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.

End abstraction_equivalence_properties.

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

Fixpoint ones_late_opt (a:abstractionj) (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 (absj_r a * i + absj_b0 a) ones_i' with
      | Lt | Eq => Some (ones_i')
      | Gt =>
        match Qcompare ones_i' (absj_r a * i + absj_b1 a) with
        | Lt => Some (S ones_i')
        | Gt | Eq => None
        end
      end
    end
  end.

Definition non_empty_alt (a: abstractionj) :=
  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 ones_early a i' ?= absj_r a * S i' + absj_b1 a with
     | Eq => 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 absj_r a * (S i') + absj_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 ones_i' (absj_r a * S i' + absj_b1 a) with
       | Lt => Some (S ones_i')
       | Gt | Eq =>
         match Qcompare (absj_r a * S i' + absj_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 (absj_r a * S i' + absj_b0 a) ones_i' with
       | Lt | Eq => Some (ones_i')
       | Gt =>
         match Qcompare ones_i' (absj_r a * S i' + absj_b1 a) with
         | Lt => Some (S ones_i')
         | Gt | Eq => None
         end
       end
     end)%nat.
  Proof.
    intros.
    simpl.
    reflexivity.
  Qed.

  Lemma ones_early_alt_remove_Zabs_nat:
    forall a:abstractionj,
    forall i,
    ((Z_of_nat (ones_early_alt a i))%Z =
      Zmax O (Zmin i (cg (absj_r a * i + absj_b1 a))))%Z.
  Proof.
    intros.
    unfold ones_early_alt.
    rewrite inj_Zabs_nat.
    elim (Zabs_spec (Zmax O (Zmin i (cg (absj_r a * i + absj_b1 a))))).
      intro H_tmp; destruct H_tmp.
      rewrite H0.
      reflexivity.
      intro H_tmp; destruct H_tmp.
      elim (Zmax_spec O (Zmin i (cg (absj_r a * i + absj_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:abstractionj,
    forall i,
    ((Z_of_nat (ones_late_alt a i))%Z =
      Zmax O (Zmin i (cg (absj_r a * i + absj_b0 a))))%Z.
  Proof.
    intros.
    unfold ones_late_alt.
    rewrite inj_Zabs_nat.
    elim (Zabs_spec (Zmax O (Zmin i (cg (absj_r a * i + absj_b0 a))))).
      intro H_tmp; destruct H_tmp.
      rewrite H0.
      reflexivity.
      intro H_tmp; destruct H_tmp.
      elim (Zmax_spec O (Zmin i (cg (absj_r a * i + absj_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: abstractionj,
    well_formed_ones (ones_early a).
  Proof.
    intros.
    split.
      simpl.
      reflexivity.

      intro.
      simpl.
      case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a).
        intro H_cmp.
        right.
        reflexivity.

        intro H_cmp.
        left.
        reflexivity.

        intro H_cmp.
        right.
        reflexivity.
  Qed.

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

      intro.
      simpl.
      case_eq (absj_r a * S i + absj_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: abstractionj,
    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 (0%nat ?= absj_r a * 1%nat + absj_b1 a);
          intros;
          simpl;
          reflexivity.

        assert (H_aux:
          (ones_early a (S (S i'))
           =
           match ones_early a (S i') ?= absj_r a * (S (S i')) + absj_b1 a with
           | Eq => 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 ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a with
               | Eq => 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 (ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a).
          intro.
          assert (H_aux:
            beq_nat ((ones_early a (S i'))) (ones_early a (S i')) = true).
            rewrite (beq_nat_refl (ones_early a (S i'))).
            reflexivity.
          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_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: abstractionj,
    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 (absj_r a * 1%nat + absj_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 absj_r a * S (S i') + absj_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 (absj_r a * S (S i') + absj_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: abstractionj,
    forall H_wf: well_formed_abstractionj 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 (cg (absj_r a * O%nat + absj_b1 a)))).
       intro H_tmp; destruct H_tmp.
       rewrite H0.
       reflexivity.

       intro H_tmp; destruct H_tmp.
       rewrite H0.
       elim (Zmin_spec 0%nat (cg (absj_r a * 0%nat + absj_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) (cg (absj_r a * S i + absj_b1 a)))).
       intro H_tmp; destruct H_tmp.
       elim (Zmin_spec (S i) (cg (absj_r a * (S i) + absj_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
                 (cg (absj_r a * S i + absj_b1 a))
                 (cg (absj_r a * i + absj_b1 a))); auto.
             apply Zle_ge.
             apply cg_monotone_linear.
             assert (H_aux:
               absj_r a * i + absj_b1 a ==
               absj_r a * i + absj_b1 a + 0).
               ring.
             rewrite H_aux; clear H_aux.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               absj_r a * (i + 1) + absj_b1 a ==
               absj_r a * i + absj_b1 a + absj_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 (absj_r a * S i + absj_b1 a))
               (cg (absj_r a * i + absj_b1 a))); auto.
             apply cg_monotone_linear.
             assert (H_aux:
               absj_r a * i + absj_b1 a ==
               absj_r a * i + absj_b1 a + 0).
               ring.
             rewrite H_aux; clear H_aux.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               absj_r a * (i + 1) + absj_b1 a ==
               absj_r a * i + absj_b1 a + absj_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: ones_early a i >= absj_r a * S i + absj_b1 a).
           clear H0; clear H2.
           rewrite H_cc_aux1.
           apply (Qle_trans
             (absj_r a * S i + absj_b1 a)
             (cg(absj_r a * S i + absj_b1 a))
             0).
           destruct (cg_def_linear (absj_r a * S i + absj_b1 a)); assumption.
           apply Zle_impl_Qle.
           apply Zge_le.
           assumption.

         rewrite red_ones_early.
         case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a);
           try solve [ intro H_cmp; apply inj_eq; assumption].
         intro H_cmp.
         rewrite <- Qlt_alt in H_cmp.
         absurd (ones_early a i < absj_r a * S i + absj_b1 a); auto.
         apply Qle_not_lt.
         assumption.

       intro H_tmp; destruct H_tmp.
       elim (Zmin_spec (S i) (cg (absj_r a * (S i) + absj_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)
             (cg (absj_r a * i + absj_b1 a) + 1)).
             apply inj_lt.
             auto with arith.
             rewrite <- cg_plus_int_rewrite.
             apply (Zle_trans
               (S i)
               (cg (absj_r a * S i + absj_b1 a))
               (cg (absj_r a * i + absj_b1 a + 1))); auto.
             apply cg_monotone_linear.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               absj_r a * (i + 1) + absj_b1 a ==
               absj_r a * i + absj_b1 a + absj_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: ones_early a i < absj_r a * S i + absj_b1 a).
           rewrite H_cc_aux1.
           apply (Qle_lt_trans
             i
             (cg (absj_r a * S i + absj_b1 a) - 1)%Z
             (absj_r a * S i + absj_b1 a));
           try solve [ elim (cg_def_linear (absj_r a * S i + absj_b1 a));
                       intros; assumption ].
           assert (H_aux:
             (cg (absj_r a * S i + absj_b1 a) - 1%nat) ==
             (cg (absj_r a * S i + absj_b1 a) - 1%nat)%Z).
             unfold Qeq; simpl; omega.
           rewrite <- H_aux; clear H_aux.
           unfold Qminus.
           rewrite -> Qle_minus_iff.
           assert (H_aux:
             cg (absj_r a * S i + absj_b1 a) + - (1) + - i ==
             cg (absj_r a * S i + absj_b1 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_early.
         rewrite Qlt_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_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: ones_early a i < absj_r a * S i + absj_b1 a).
             rewrite Qlt_alt.
             case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a); auto;
               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_le_trans
                 (ones_early_alt a i)
                 (absj_r a * S i + absj_b1 a)
                 (cg (absj_r a * S i + absj_b1 a))); auto.
             elim (cg_def_linear (absj_r a * S i + absj_b1 a)); auto.

             rewrite ones_early_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:
                   absj_r a * (i + 1) + absj_b1 a ==
                   absj_r a * i + absj_b1 a + absj_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 (absj_r a * S i + absj_b1 a))
                     (cg (absj_r a * i + absj_b1 a) + 1%nat)); auto.
                 rewrite <- cg_plus_int_rewrite.
                 apply cg_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   absj_r a * (i + 1) + absj_b1 a ==
                   absj_r a * i + absj_b1 a + absj_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 (absj_r a * S i + absj_b1 a))
                   (cg (absj_r a * i + absj_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 cg_monotone_linear.
                 apply Qplus_le_compat; try solve [ apply Qle_refl ].
                 rewrite Qmult_comm.
                 assert (H_aux: absj_r a * S i == S i * absj_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: ones_early a i >= absj_r a * S i + absj_b1 a).
             rewrite Qge_alt.
             case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a).
               intro H_cmp.
               intro.
               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.
               intro.
               congruence.
           rewrite IHi in H_cmp.
           apply Zle_antisym.
             rewrite ones_early_alt_remove_Zabs_nat.
             rewrite Zmin_right; auto.
               rewrite Zmax_right.
                 apply cg_monotone_linear.
                 assert (H_aux:
                   absj_r a * i + absj_b1 a ==
                   absj_r a * i + absj_b1 a + 0).
                   ring.
                 rewrite H_aux; clear H_aux.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   absj_r a * (i + 1) + absj_b1 a ==
                   absj_r a * i + absj_b1 a + absj_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 (absj_r a * S i + absj_b1 a))
                     (cg (absj_r a * i + absj_b1 a) + 1%nat)); auto.
                 rewrite <- cg_plus_int_rewrite.
                 apply cg_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   absj_r a * (i + 1) + absj_b1 a ==
                   absj_r a * i + absj_b1 a + absj_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 (absj_r a * S i + absj_b1 a))
                   (cg (absj_r a * i + absj_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 cg_monotone_linear.
                 apply Qplus_le_compat; try solve [ apply Qle_refl ].
                 rewrite Qmult_comm.
                 assert (H_aux: absj_r a * S i == S i * absj_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.

  Property ones_late_eq_ones_late_alt:
    forall a: abstractionj,
    forall H_wf: well_formed_abstractionj 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 (absj_r a * O%nat + absj_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 (absj_r a * 0%nat + absj_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 (absj_r a * S i + absj_b0 a)))).
       intro H_tmp; destruct H_tmp.
       elim (Zmin_spec (S i) (cg (absj_r a * (S i) + absj_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 (absj_r a * S i + absj_b0 a))
                 (cg (absj_r a * i + absj_b0 a))); auto.
             apply Zle_ge.
             apply cg_monotone_linear.
             assert (H_aux:
               absj_r a * i + absj_b0 a ==
               absj_r a * i + absj_b0 a + 0).
               ring.
             rewrite H_aux; clear H_aux.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               absj_r a * (i + 1) + absj_b0 a ==
               absj_r a * i + absj_b0 a + absj_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 (absj_r a * S i + absj_b0 a))
               (cg (absj_r a * i + absj_b0 a))); auto.
             apply cg_monotone_linear.
             assert (H_aux:
               absj_r a * i + absj_b0 a ==
               absj_r a * i + absj_b0 a + 0).
               ring.
             rewrite H_aux; clear H_aux.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               absj_r a * (i + 1) + absj_b0 a ==
               absj_r a * i + absj_b0 a + absj_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: absj_r a * S i + absj_b0 a <= ones_late a i).
           clear H0; clear H2.
           rewrite H_cc_aux1.
           apply (Qle_trans
             (absj_r a * S i + absj_b0 a)
             (cg(absj_r a * S i + absj_b0 a))
             0).
           destruct (cg_def_linear (absj_r a * S i + absj_b0 a)); assumption.
           apply Zle_impl_Qle.
           apply Zge_le.
           assumption.

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

       intro H_tmp; destruct H_tmp.
       elim (Zmin_spec (S i) (cg (absj_r a * (S i) + absj_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 (absj_r a * i + absj_b0 a) + 1)).
             apply inj_lt.
             auto with arith.
             rewrite <- cg_plus_int_rewrite.
             apply (Zle_trans
               (S i)
               (cg (absj_r a * S i + absj_b0 a))
               (cg (absj_r a * i + absj_b0 a + 1))); auto.
             apply cg_monotone_linear.
             rewrite <- n_plus_1_eq_S_n.
             assert (H_aux:
               absj_r a * (i + 1) + absj_b0 a ==
               absj_r a * i + absj_b0 a + absj_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: absj_r a * S i + absj_b0 a > ones_late a i).
           rewrite H_cc_aux1.
           apply (Qle_lt_trans
             i
             (cg (absj_r a * S i + absj_b0 a) - 1)%Z
             (absj_r a * S i + absj_b0 a));
           try solve [ elim (cg_def_linear (absj_r a * S i + absj_b0 a));
                       intros; assumption ].
           assert (H_aux:
             (cg (absj_r a * S i + absj_b0 a) - 1%nat) ==
             (cg (absj_r a * S i + absj_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 (absj_r a * S i + absj_b0 a) + - (1) + - i ==
             cg (absj_r a * S i + absj_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: absj_r a * S i + absj_b0 a > ones_late a i).
             rewrite Qlt_alt.
             case_eq (absj_r a * S i + absj_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)
                 (absj_r a * S i + absj_b0 a)
                 (cg (absj_r a * S i + absj_b0 a))); auto.
             elim (cg_def_linear (absj_r a * S i + absj_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:
                   absj_r a * (i + 1) + absj_b0 a ==
                   absj_r a * i + absj_b0 a + absj_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 (absj_r a * S i + absj_b0 a))
                     (cg (absj_r a * i + absj_b0 a) + 1%nat)); auto.
                 rewrite <- cg_plus_int_rewrite.
                 apply cg_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   absj_r a * (i + 1) + absj_b0 a ==
                   absj_r a * i + absj_b0 a + absj_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 (absj_r a * S i + absj_b0 a))
                   (cg (absj_r a * i + absj_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: absj_r a * S i == S i * absj_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: absj_r a * S i + absj_b0 a <= ones_late a i).
             rewrite Qge_alt.
             case_eq (absj_r a * S i + absj_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 < absj_r a * S i + absj_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:
                   absj_r a * i + absj_b0 a ==
                   absj_r a * i + absj_b0 a + 0).
                   ring.
                 rewrite H_aux; clear H_aux.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   absj_r a * (i + 1) + absj_b0 a ==
                   absj_r a * i + absj_b0 a + absj_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 (absj_r a * S i + absj_b0 a))
                     (cg (absj_r a * i + absj_b0 a) + 1%nat)); auto.
                 rewrite <- cg_plus_int_rewrite.
                 apply cg_monotone_linear.
                 rewrite <- n_plus_1_eq_S_n.
                 assert (H_aux:
                   absj_r a * (i + 1) + absj_b0 a ==
                   absj_r a * i + absj_b0 a + absj_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 (absj_r a * S i + absj_b0 a))
                   (cg (absj_r a * i + absj_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: absj_r a * S i == S i * absj_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_i_lt_a:
    forall a i,
    forall H_w: w_early a (S i) = true,
    ones (w_early a) i < (absj_r a * S i + absj_b1 a).
  Proof.
    intros.
    simpl in H_w.
    case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a).
      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 <- Qlt_alt in H_cmp.
      rewrite ones_early_eq_ones_w_early in H_cmp.
      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_ge_a:
    forall a i,
    forall H_w: w_early a (S i) = false,
    ones (w_early a) i >= (absj_r a * S i + absj_b1 a).
  Proof.
    intros.
    simpl in H_w.
    case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a).
      intro H_cmp.
      rewrite <- Qeq_alt in H_cmp.
      rewrite ones_early_eq_ones_w_early in H_cmp.
      rewrite H_cmp.
      apply Qle_refl.

      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 <- Qgt_alt in H_cmp.
      rewrite ones_early_eq_ones_w_early in H_cmp.
      apply Qlt_le_weak.
      assumption.
  Qed.

  Property ones_w_le_ones_early:
    forall w: ibw,
    forall a: abstractionj,
    forall H_wf_a: well_formed_abstractionj a,
    forall H_w_in_a: in_abstractionj 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 (0%nat ?= absj_r a * 1%nat + absj_b1 a);
          try solve [ intros; apply le_refl ].
          intros H_cmp.
          rewrite <- Qeq_alt in H_cmp.
          absurd (0 == absj_r a * 1 + absj_b1 a); auto.
          apply Qlt_not_eq.
          assumption.
          intros H_cmp.
          rewrite <- Qgt_alt in H_cmp.
          absurd (absj_r a * 1 + absj_b1 a < 0); auto.
          apply Qle_not_lt.
          apply Qlt_le_weak.
          assumption.

        intro H_w.

        simpl.
        rewrite H_w.
        simpl.
        case_eq (0%nat ?= absj_r a * 1%nat + absj_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 ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a with
               | Eq => (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 (ones_early a (S i') ?= absj_r a * S (S i') + absj_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.
            change (pred (S (S i'))) with (S i') in H_ones_le_a.
            rewrite H_cmp in H_ones_le_a.
            assert (H_aux:
              (ones_early a (S (S i'))
               =
               match ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a with
               | Eq => 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 (ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a);
              try omega.
              intro H_cmp'.
              rewrite <- Qeq_alt in H_cmp'.
              rewrite <- H_cmp' in H_ones_le_a.
              absurd (ones_early a (S i') < ones_early a (S i')); auto.
              apply Qle_not_lt.
              apply Qle_refl.

              intro H_cmp'.
              rewrite <- Qgt_alt in H_cmp'.
              absurd (absj_r a * S (S i') + absj_b1 a < ones_early a (S i')); auto.
              apply Qle_not_lt.
              apply Qlt_le_weak.
              assumption.

        intro H_w.
        rewrite ones_S_i_eq_ones_i; auto.
        assert (H_aux:
          (ones_early a (S (S i'))
           =
           match ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a with
           | Eq => 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 (ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a);
        omega.
  Qed.

  Property ones_late_le_ones_w:
    forall w: ibw,
    forall a: abstractionj,
    forall H_wf_a: well_formed_abstractionj a,
    forall H_w_in_a: in_abstractionj 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 (absj_r a * 1%nat + absj_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 (absj_r a * 1%nat + absj_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 < absj_r a * 1 + absj_b0 a); auto.
        apply Qle_not_lt.
        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 (absj_r a * S (S i') + absj_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 (absj_r a * S (S i') + absj_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'))
            (absj_r a * S (S i') + absj_b0 a)
            (ones w (S i')));
          try solve [ exact H_cmp ].
        unfold in_abstractionj in H_w_in_a.
        replace (ones w (S i')) with (ones w (pred (S (S i')))); auto.
        apply (H_w_in_a (S (S i'))); auto with arith.
  Qed.

  Lemma ones_early_opt_impl_ones_early:
   forall a: abstractionj,
   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 (ones_early a i ?= absj_r a * S i + absj_b1 a);
        try reflexivity.
        intro H_cmp.
        case_eq (absj_r a * S i + absj_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.

        intro H_cmp.
        case_eq (absj_r a * S i + absj_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: abstractionj,
   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 (absj_r a * S i + absj_b0 a ?= ones_late a i);
        try reflexivity.
        intro H_cmp.
        case_eq (ones_late a i ?= absj_r a * S i + absj_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.

          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: abstractionj,
    forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
    forall H_absj_b1_lt_absj_b0: absj_b1 a < absj_b0 a,
    forall i,
    ones_late a i = ones_early a i.
  Proof.
    induction i.
      simpl.
      reflexivity.

      simpl.
      case_eq (absj_r a * S i + absj_b0 a ?= ones_late a i).
        intros H_cmp_zero.
        rewrite IHi.
        case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a).
          intros H_cmp_one.
          rewrite <- Qeq_alt in *.
          rewrite IHi in H_cmp_zero.
          rewrite H_cmp_one in H_cmp_zero.
          apply Qeq_sym in H_cmp_zero.
          absurd (absj_r a * S i + absj_b1 a == absj_r a * S i + absj_b0 a);
            auto.
          apply Qlt_not_eq.
          apply Qplus_lt_compat_l.
          assumption.

          intros H_cmp_one.
          rewrite <- Qeq_alt in *.
          rewrite <- Qlt_alt in *.
          absurd (ones_early a i < absj_r a * S i + absj_b1 a);
            auto.
          rewrite IHi in H_cmp_zero.
          rewrite <- H_cmp_zero.
          apply Qle_not_lt.
          apply Qplus_le_compat; try solve [apply Qle_refl; auto].
          apply Qlt_le_weak.
          assumption.

          reflexivity.

        intros H_cmp_zero.
        rewrite IHi.
        case_eq (ones_early a i ?= absj_r a * S i + absj_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.
          rewrite H_cmp_one in H_cmp_zero.
          absurd (absj_r a * S i + absj_b0 a < absj_r a * S i + absj_b1 a);
            auto.
          apply Qle_not_lt.
          apply Qplus_le_compat; try solve [apply Qle_refl; auto].
          apply Qlt_le_weak.
          assumption.

          intros H_cmp_one.
          rewrite <- Qlt_alt in *.
          absurd (absj_r a * S i + absj_b0 a < absj_r a * S i + absj_b1 a).
            apply Qle_not_lt.
            apply Qplus_le_compat; try solve [apply Qle_refl; auto].
            apply Qlt_le_weak.
            assumption.

            rewrite IHi in H_cmp_zero.
            apply
              (Qlt_trans
                (absj_r a * S i + absj_b0 a)
                (ones_early a i)
                (absj_r a * S i + absj_b1 a)); auto.

          reflexivity.

        intros H_cmp_zero.
        rewrite IHi.
        case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a).
          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.

          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: abstractionj,
    forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
    in_abstractionj (w_early a) a.
  Proof.
    intros.
    unfold in_abstractionj.
    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_i_lt_a.
        exact H_w_early_S_i'.

        intro H_w_early_S_i'.
        assert (H_cmp: (absj_r a * S i' + absj_b1 a) <= (ones_early a i')).
          rewrite ones_early_eq_ones_w_early.
          apply w_early_S_i_eq_false_impl_ones_early_i_ge_a; auto.
        rewrite Qge_alt in H_cmp.
        pose (H_non_empty_i:=H_non_empty (S i')).
        assert (H_aux: (ones_early a (S i') = ones_early a i')%nat).
          simpl.
          case_eq (ones_early a i' ?= absj_r a * S i' + absj_b1 a);
            try reflexivity.
          intros.
          congruence.
        rewrite H_aux in H_non_empty_i.
        simpl in H_non_empty_i.
        case_eq (absj_r a * S i' + absj_b0 a ?= ones_late a i').
          intro H_cmp'.
          rewrite H_cmp' in *.
          rewrite <- Qeq_alt in H_cmp'.
          rewrite H_cmp'.
          apply le_impl_Qle.
          simpl.
          rewrite <- ones_early_eq_ones_w_early.
          exact H_non_empty_i.

          intro H_cmp'.
          rewrite <- Qlt_alt in H_cmp'.
          simpl.
          rewrite <- ones_early_eq_ones_w_early.
          apply
            (Qle_trans
              (absj_r a * S i' + absj_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 (absj_b1 a) (absj_b0 a)).
              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.
              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
                  (absj_r a * S (S i'') + absj_b0 a)
                  (absj_r a * S (S i'') + absj_b1 a)
                  (ones_early a (S i'')));
                try solve [
                  apply Qplus_le_compat; auto;
                   apply Qle_refl].
              rewrite <- Qge_alt in H_cmp.
              assumption.
  Qed.

  Property ones_late_le_ones_early_impl_late_in_a:
    forall a: abstractionj,
    forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
    in_abstractionj (w_late a) a.
  Proof.
    intros.
    unfold in_abstractionj.
    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 (absj_r a * S i' + absj_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 (ones_early a i' ?= absj_r a * S i' + absj_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 lt_impl_Qlt.
            apply le_lt_n_Sm in H_non_empty_i.
            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.
            apply (Qle_lt_trans
                (ones_late a i')
                (ones_early a i')
                (absj_r a * S i' + absj_b1 a)); 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 (absj_b1 a) (absj_b0 a)).
              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.
              apply (Qlt_le_trans
                (ones_late a i')
                (absj_r a * S i' + absj_b0 a)
                (absj_r a * S i' + absj_b1 a)); auto.
              apply Qplus_le_compat; try solve [ apply Qle_refl ].
              assumption.

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

          intro H_cmp.
          rewrite <- Qlt_alt in H_cmp.
          apply Qlt_le_weak.
          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: abstractionj,
    forall H_wf: well_formed_abstractionj 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: abstractionj,
    forall H_wf: well_formed_abstractionj a,
    forall H_non_empty: non_empty a,
    in_abstractionj (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: abstractionj,
    forall H_wf: well_formed_abstractionj a,
    forall H_non_empty: non_empty a,
    in_abstractionj (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.

End early_and_late_properties.

Lemma ones_late_le_ones_early_impl_non_empty:
  forall a,
  forall H_wf: well_formed_abstractionj 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:
    forall a,
    forall H_wf: well_formed_abstractionj a,
    forall H_non_empty: non_empty_test a,
    forall i,
    (ones_late a i <= ones_early a i)%nat.
  Proof.
    intros.
    unfold non_empty_test in 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.
    apply cg_monotone_linear.
    apply Qplus_le_compat; try solve [ apply Qle_refl ].
    assumption.
  Qed.

End non_empty_test_properties.


Section std_properties.

  Lemma absj_std_red:
    forall a: abstractionj,
    absj_std a =
    absjmake
      (absj_b1 a * (QDen (absj_r a) # Qden (absj_r a)))
      (absj_b0 a)
      (absj_r a * (QDen (absj_b1 a) # Qden (absj_b1 a))).
  Proof.
    intros.
    reflexivity.
  Qed.

  Property absj_std_correctness:
    forall a: abstractionj,
    absj_equal a (absj_std a).
  Proof.
    intros a.
    rewrite absj_std_red.
    repeat split.
      simpl.
      assert (H_aux: (' Qden (absj_b1 a) # Qden (absj_b1 a)) == 1).
        unfold Qeq.
        simpl.
        rewrite Pmult_1_r.
        reflexivity.
      rewrite H_aux; clear H_aux.
      rewrite Qmult_1_r.
      reflexivity.
      simpl.
      assert (H_aux: (' Qden (absj_r a) # Qden (absj_r a)) == 1).
        unfold Qeq.
        simpl.
        rewrite Pmult_1_r.
        reflexivity.
      rewrite H_aux; clear H_aux.
      rewrite Qmult_1_r.
      reflexivity.
  Qed.

  Property absj_std_well_formed_abstractionj_compat:
    forall a: abstractionj,
    forall H_wf: well_formed_abstractionj a,
    well_formed_abstractionj (absj_std a).
  Proof.
    intros.
    unfold well_formed_abstractionj in *.
    rewrite absj_std_red.
    simpl.
    assert (H_aux: (' Qden (absj_b1 a) # Qden (absj_b1 a)) == 1).
      unfold Qeq.
      simpl.
      rewrite Pmult_1_r.
      reflexivity.
    rewrite H_aux; clear H_aux.
    rewrite Qmult_1_r.
    assumption.
  Qed.

  Property absj_std_in_abstractionj_compat:
    forall w: ibw,
    forall a: abstractionj,
    forall H_w_in_a: in_abstractionj w a,
    in_abstractionj w (absj_std a).
  Proof.
    intros.
    rewrite absj_std_red.
    unfold in_abstractionj.
    simpl.
    intros.
    assert (H_aux: (' Qden (absj_b1 a) # Qden (absj_b1 a)) == 1).
      unfold Qeq.
      simpl.
      rewrite Pmult_1_r.
      reflexivity.
    rewrite H_aux; clear H_aux.
    assert (H_aux: (' Qden (absj_r a) # Qden (absj_r a)) == 1).
      unfold Qeq.
      simpl.
      rewrite Pmult_1_r.
      reflexivity.
    rewrite H_aux; clear H_aux.
    repeat rewrite Qmult_1_r.
    pose (H_cc := H_w_in_a i H_i_ge_1).
    assumption.
  Qed.

End std_properties.


Section on_properties.

  Lemma on_w1_w2_lt_on_a1_a2:
    forall (w1:ibw) (w2:ibw),
    forall (a1:abstractionj) (a2:abstractionj),
    forall H_wf_a1: well_formed_abstractionj a1,
    forall H_wf_a2: well_formed_abstractionj a2,
    forall (H_a1_eq_absj_w1: in_abstractionj w1 a1),
    forall (H_a2_eq_absj_w2: in_abstractionj w2 a2),
    forall H_wf_b1_1: Qden (absj_b1 a1) = Qden (absj_r a1),
    forall H_wf_b1_2: Qden (absj_b1 a2) = Qden (absj_r a2),
    forall epsilon: Q,
    forall H_epsilon: epsilon == (1 - (1 # Qden (absj_r a1) )) * ((absj_r a2) - (1 # Qden (absj_r a2))),
    forall i,
    forall H_i_ge_1: (i >= 1)%nat,
    forall (H_on: on w1 w2 i = true),
    ones (on w1 w2) (pred i) <
    (absj_r a1 * absj_r a2) * i + ((absj_b1 a1 * absj_r a2 + absj_b1 a2) + epsilon).
  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 (pred i) < absj_r a1 * i + absj_b1 a1).
      unfold in_abstractionj in H_a1_eq_absj_w1.
      generalize (H_a1_eq_absj_w1 i H_i_ge_1).
      clear H_a1_eq_absj_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 (pred (ones w1 i)) < (absj_r a2 * ones w1 i + absj_b1 a2)).
      unfold in_abstractionj in H_a2_eq_absj_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_absj_w2 (ones w1 i) H_ones_w1_ge_1).
      clear H_a2_eq_absj_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.

    assert (H_aux: ones w1 (pred i) = pred (ones w1 i)).
      apply ones_pred_i_eq_pred_ones_i; assumption.
    rewrite H_aux; rewrite H_aux in H_w1_le_a1; clear H_aux.

    assert (H_aux: pred (ones w1 i) == ones w1 i - 1).
      case_eq (ones w1 i).
        intro H_ones_w1.
        absurd (O = ones w1 i); auto.
        apply lt_O_neq.
        apply w_i_eq_true_impl_ones_pos; auto.

        intros.
        rewrite <- n_plus_1_eq_S_n.
        simpl.
        assert (H_aux: n + 1 - 1 == n).
          ring.
        rewrite H_aux; clear H_aux.
        apply Qeq_refl.
    rewrite H_aux in H_w1_le_a1; clear H_aux.
    assert (H_aux: ones w1 i - 1 == - (1) + ones w1 i).
      ring.
    rewrite H_aux in H_w1_le_a1; clear H_aux.
    assert (H_aux:
      absj_r a1 * i + absj_b1 a1 ==
      - (1) + (absj_r a1 * i + absj_b1 a1 + 1)).
      ring.
    rewrite H_aux in H_w1_le_a1; clear H_aux.
    rewrite Qlt_plus in H_w1_le_a1.

    assert (H_tmp:
      absj_r a1 * i + absj_b1 a1 + 1 ==
      absj_r a1 * i + (Qnum (absj_b1 a1) + QDen (absj_b1 a1)) / (QDen (absj_b1 a1))).
      rewrite <- Qplus_assoc.
      apply Qplus_eq_compat; try solve [ apply Qeq_refl ].
      unfold Qplus, Qeq, Q_of_nat, Qdiv; simpl; ring_simplify; simpl.
      rewrite Pmult_1_r. reflexivity.
    rewrite H_tmp in H_w1_le_a1.
    assert (H_den:
      1 # Qden (absj_r a1) <= 1 # Qden (Qred (absj_r a1 * i + ((Qnum (absj_b1 a1) + QDen (absj_b1 a1)) / (QDen (absj_b1 a1)))))).
      apply den_r_le_den_r_i_p_b.
      assumption.
    apply
      (Qlt_impl_Qle_red (ones w1 i) (absj_r a1 * i + (((Qnum (absj_b1 a1) + QDen (absj_b1 a1)) / (QDen (absj_b1 a1)))))
        (1 # Qden (absj_r a1)) H_den) in H_w1_le_a1.
    clear H_den.

    rewrite <- H_tmp in H_w1_le_a1.
    assert (H_den:
      1 # Qden (absj_r a2) <= 1 # Qden (Qred (absj_r a2 * ones w1 i + absj_b1 a2))).
      apply den_r_le_den_r_i_p_b.
      assumption.
    apply
      (Qlt_impl_Qle_red (ones w2 (pred (ones w1 i))) (absj_r a2 * ones w1 i + absj_b1 a2)
        (1 # Qden (absj_r a2)) H_den) in H_w2_le_a2.
    clear H_den.
    apply
      (Qle_lt_trans
        (ones w2 (pred (ones w1 i)))
        (Qred (absj_r a2 * ones w1 i + absj_b1 a2) - (1 # Qden (absj_r a2)))
        (absj_r a1 * absj_r a2 * i + (absj_b1 a1 * absj_r a2 + absj_b1 a2 + epsilon)));
      auto.
    apply (Qle_lt_trans
      (Qred (absj_r a2 * ones w1 i + absj_b1 a2) - (1 # Qden (absj_r a2)))
      (Qred (absj_r a2 * (Qred (absj_r a1 * i + absj_b1 a1 + 1) - (1 # Qden (absj_r a1))) + absj_b1 a2) - (1 # Qden (absj_r a2)))
      (absj_r a1 * absj_r a2 * i + (absj_b1 a1 * absj_r a2 + absj_b1 a2 + epsilon))).
      apply Qplus_le_compat; try solve [ apply Qle_refl ].
      repeat rewrite Qred_correct.
      apply Qplus_le_compat; try solve [ apply Qle_refl ].
      repeat rewrite (Qmult_comm (absj_r a2)).
      apply Qmult_le_compat_r.
      2: (destruct H_wf_a2; auto).
      rewrite Qred_correct in H_w1_le_a1.
      assumption.
      repeat rewrite Qred_correct.
      assert (H_aux:
        absj_r a2 * (absj_r a1 * i + absj_b1 a1 + 1 - (1 # Qden (absj_r a1))) +
        absj_b1 a2 - (1 # Qden (absj_r a2))
        ==
        (absj_r a1 * absj_r a2 * i + absj_b1 a1 * absj_r a2 + absj_b1 a2)
        + (absj_r a2 * (1 - (1 # Qden (absj_r a1))) - (1 # Qden (absj_r a2)))).
        ring.
      rewrite H_aux; clear H_aux.
      assert (H_aux:
        absj_r a1 * absj_r a2 * i + (absj_b1 a1 * absj_r a2 + absj_b1 a2 + epsilon) ==
        (absj_r a1 * absj_r a2 * i + absj_b1 a1 * absj_r a2 + absj_b1 a2) + epsilon).
        ring.
      rewrite H_aux; clear H_aux.
      apply Qplus_lt_compat_l.
      rewrite H_epsilon.
      assert (H_aux:
        (1 - (1 # Qden (absj_r a1))) * (absj_r a2 - (1 # Qden (absj_r a2))) ==
        absj_r a2 * (1 - (1 # Qden (absj_r a1))) - (1 # Qden (absj_r a2)) * (1 - (1 # Qden (absj_r a1)))).
        ring.
      rewrite H_aux; clear H_aux.
      apply Qplus_lt_compat_l.
      apply Qround.Qopp_lt_compat.
      rewrite <- (Qmult_1_r (1 # Qden (absj_r a2))) at 2.
      repeat rewrite (Qmult_comm (1 # Qden (absj_r a2))).
      apply Qmult_lt_compat_r.
        unfold Qlt; simpl; ring_simplify; simpl; auto with zarith.
        apply <- Qlt_minus_iff.
        assert (H_aux:
          1 + - (1 - (1 # Qden (absj_r a1))) ==
          1 # Qden (absj_r a1)).
          ring.
        rewrite H_aux; clear H_aux.
        unfold Qlt; simpl; ring_simplify; simpl; auto with zarith.

  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 absj_b0_neg_impl_ones_ge_a:
    forall (w:ibw) (a:abstractionj),
    forall H_wf_a: well_formed_abstractionj a,
    forall H_flo: absj_b0 a <= 0,
    forall H_a_eq_absj_w: in_abstractionj w a,
    forall i:nat,
    ones w i >= absj_r a * i + absj_b0 a.
  Proof.
    induction i.
      assert (H_aux: absj_r a * 0 == 0).
        ring.
      rewrite H_aux; clear H_aux.
      assert (H_aux: 0 + absj_b0 a == absj_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:
          absj_r a * (i + 1) + absj_b0 a ==
          absj_r a * i + absj_b0 a + absj_r a).
          ring.
        rewrite H_aux; clear H_aux.
        apply Qplus_le_compat; try solve [ elim H_wf_a; auto ].

        intro H_w.
        unfold in_abstractionj in H_a_eq_absj_w.
        assert (H_S_i_ge_1:(S i >= 1)%nat).
          auto with arith.
        generalize (H_a_eq_absj_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.
        replace (pred (S i)) with i; auto.
        rewrite ones_S_i_eq_ones_i; auto.
  Qed.

  Lemma on_w1_w2_ge_on_a1_a2:
    forall (w1:ibw) (w2:ibw),
    forall (a1:abstractionj) (a2:abstractionj),
    forall H_wf_a1: well_formed_abstractionj a1,
    forall H_flo_a1: absj_b0 a1 <= 0,
    forall H_wf_a2: well_formed_abstractionj a2,
    forall H_flo_a2: absj_b0 a2 <= 0,
    forall (H_a1_eq_absj_w1: in_abstractionj w1 a1),
    forall (H_a2_eq_absj_w2: in_abstractionj w2 a2),
    forall i,
    forall (H_on: on w1 w2 i = false),
     absj_r a1 * absj_r a2 * i + (absj_b0 a1 * absj_r a2 + absj_b0 a2)
     <= ones (on w1 w2) i.
  Proof.
    intros.
    rewrite ones_on_def.
    generalize (absj_b0_neg_impl_ones_ge_a H_wf_a1 H_flo_a1 H_a1_eq_absj_w1 i).
    intro H_w1_ge_a1.
    generalize (absj_b0_neg_impl_ones_ge_a H_wf_a2 H_flo_a2 H_a2_eq_absj_w2 (ones w1 i)).
    intro H_w2_ge_a2.
    apply
      (Qle_trans
        (absj_r a1 * absj_r a2 * i + (absj_b0 a1 * absj_r a2 + absj_b0 a2))
        (absj_r a2 * ones w1 i + absj_b0 a2)
        (ones w2 (ones w1 i))); auto.
    rewrite Qplus_assoc.
    apply Qplus_le_compat; try solve [ apply Qle_refl ].
    assert (H_r2_pos: 0 <= absj_r a2);
      destruct H_wf_a2; auto.
    generalize
      (Qmult_le_compat_r
        (absj_r a1 * i + absj_b0 a1)
        (ones w1 i)
        (absj_r a2)
        H_w1_ge_a1
        H_r2_pos).
    intro H_cc.
    rewrite Qmult_plus_distr_l in H_cc.
    assert (H_aux: absj_r a1 * i * absj_r a2 == absj_r a1 * absj_r a2 * i).
      ring.
    rewrite H_aux in H_cc; clear H_aux.
    assert (H_aux: ones w1 i * absj_r a2 == absj_r a2 * ones w1 i).
      ring.
    rewrite H_aux in H_cc; clear H_aux.
    exact H_cc.
  Qed.

  Property on_absj_alt_correctness_aux:
    forall (w1:ibw) (w2:ibw),
    forall (a1:abstractionj) (a2:abstractionj),
    forall H_wf_a1: well_formed_abstractionj a1,
    forall H_wf_a2: well_formed_abstractionj a2,
    forall H_a1_eq_absj_w1: in_abstractionj w1 a1,
    forall H_a2_eq_absj_w2: in_abstractionj w2 a2,
    forall H_wf_b1_1: Qden (absj_b1 a1) = Qden (absj_r a1),
    forall H_wf_b1_2: Qden (absj_b1 a2) = Qden (absj_r a2),
    in_abstractionj (on w1 w2) (on_absj_alt a1 a2).
  Proof.
    intros.

    assert (H_aux:
      exists a1_0,
        (absj_b1 a1_0 == absj_b1 a1) /\
        (absj_b0 a1_0 == 0) /\
        (absj_r a1_0 == absj_r a1)).
      exists (absjmake (absj_b1 a1) 0 (absj_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_abstractionj a1_0).
      unfold well_formed_abstractionj.
      destruct H_a1_0.
      destruct H0.
      rewrite H1.
      assumption.
    assert (H_absj_b01_0: absj_b0 a1_0 <= 0).
      destruct H_a1_0.
      destruct H0.
      rewrite H0.
      eapply Qle_refl.

    assert (H_aux:
      exists a2_0,
        (absj_b1 a2_0 == absj_b1 a2) /\
        (absj_b0 a2_0 == 0) /\
        (absj_r a2_0 == absj_r a2)).
      exists (absjmake (absj_b1 a2) 0 (absj_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_abstractionj a2_0).
      unfold well_formed_abstractionj.
      destruct H_a2_0.
      destruct H0.
      rewrite H1.
      assumption.
    assert (H_absj_b02_0: absj_b0 a2_0 <= 0).
      destruct H_a2_0.
      destruct H0.
      rewrite H0.
      eapply Qle_refl.

    unfold in_abstractionj.
    intros.

    split.
      intro H_on.
      simpl.
      pose (epsilon :=
        (1 - (1 # Qden (absj_r a1))) * (absj_r a2 - (1 # Qden (absj_r a2)))).
      assert (H_epsilon:
        epsilon == (1 - (1 # Qden (absj_r a1))) * (absj_r a2 - (1 # Qden (absj_r a2)))).
        apply Qeq_refl.
      rewrite <- H_epsilon.
      eapply on_w1_w2_lt_on_a1_a2; assumption.

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

        clear H_aux1 H_aux2.
        intros H_absj_b01 H_absj_b02.
        elim (Qlt_alt (absj_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b01).
        clear H_aux1 H_aux2.
        intro H_absj_b01_eq_cmp.
        elim (Qlt_alt (absj_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b02).
        clear H_aux1 H_aux2.
        intro H_absj_b02_eq_cmp.
        simpl.
        rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.
        rewrite ones_pred_i_eq_ones_i; auto.
        apply
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 (Qlt_le_weak (absj_b0 a1) 0 H_absj_b01)
            H_wf_a2 (Qlt_le_weak (absj_b0 a2) 0 H_absj_b02)
            H_a1_eq_absj_w1 H_a2_eq_absj_w2);
          auto.

        clear H_aux1 H_aux2.
        intros H_absj_b01 H_absj_b02.
        elim (Qgt_alt (absj_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b01).
        clear H_aux1 H_aux2.
        intro H_absj_b01_eq_cmp.
        elim (Qlt_alt (absj_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b02).
        clear H_aux1 H_aux2.
        intro H_absj_b02_eq_cmp.
        simpl.
        rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.

        assert (H_a1_0_eq_absj_w1: in_abstractionj w1 a1_0).
          assert (H_a1_in_a1_0: absj_included_test a1 a1_0).
            apply absj_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_absj_w1).

        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1_0 H_absj_b01_0
            H_wf_a2 (Qlt_le_weak (absj_b0 a2) 0 H_absj_b02)
            H_a1_0_eq_absj_w1 H_a2_eq_absj_w2
            i H_on).
        decompose [and] H_a1_0.
        rewrite H2, H1.
        rewrite ones_pred_i_eq_ones_i; auto.

        clear H_aux1 H_aux2.
        intros H_absj_b01 H_absj_b02.
        elim (Qlt_alt (absj_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b01).
        clear H_aux1 H_aux2.
        intro H_absj_b01_eq_cmp.
        elim (Qgt_alt (absj_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b02).
        clear H_aux1 H_aux2.
        intro H_absj_b02_eq_cmp.
        simpl.
        rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.

        assert (H_a2_0_eq_absj_w2: in_abstractionj w2 a2_0).
          assert (H_a2_in_a2_0: absj_included_test a2 a2_0).
            apply absj_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_absj_w2).

        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 (Qlt_le_weak (absj_b0 a1) 0 H_absj_b01)
            H_wf_a2_0 H_absj_b02_0
            H_a1_eq_absj_w1 H_a2_0_eq_absj_w2
            i H_on).
        decompose [and] H_a2_0.
        rewrite H2, H1.
        rewrite ones_pred_i_eq_ones_i; auto.

        clear H_aux1 H_aux2.
        intros H_absj_b01 H_absj_b02.
        elim (Qgt_alt (absj_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b01).
        clear H_aux1 H_aux2.
        intro H_absj_b01_eq_cmp.
        elim (Qgt_alt (absj_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b02).
        clear H_aux1 H_aux2.
        intro H_absj_b02_eq_cmp.
        simpl.
        rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.

        assert (H_a1_0_eq_absj_w1: in_abstractionj w1 a1_0).
          assert (H_a1_in_a1_0: absj_included_test a1 a1_0).
            apply absj_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_absj_w1).

        assert (H_a2_0_eq_absj_w2: in_abstractionj w2 a2_0).
          assert (H_a2_in_a2_0: absj_included_test a2 a2_0).
            apply absj_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_absj_w2).

        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1_0 H_absj_b01_0
            H_wf_a2_0 H_absj_b02_0
            H_a1_0_eq_absj_w1 H_a2_0_eq_absj_w2
            i H_on).
        decompose [and] H_a1_0.
        rewrite H2, H1.
        decompose [and] H_a2_0.
        rewrite H5, H4.
        rewrite ones_pred_i_eq_ones_i; auto.

        intros H_absj_b02 H_aux.
        elim H_aux.
        clear H_aux.
        intro H_absj_b01.
        elim (Qlt_alt (absj_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b01).
        clear H_aux1 H_aux2.
        intro H_absj_b01_eq_cmp.
        elim (Qeq_alt (absj_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b02).
        clear H_aux1 H_aux2.
        intro H_absj_b02_eq_cmp.
        simpl.
        rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.
        assert (H_absj_b02_le_0: absj_b0 a2 <= 0).
          rewrite H_absj_b02.
          apply Qle_refl.
        rewrite ones_pred_i_eq_ones_i; auto.
        apply
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 (Qlt_le_weak (absj_b0 a1) 0 H_absj_b01)
            H_wf_a2 H_absj_b02_le_0
            H_a1_eq_absj_w1 H_a2_eq_absj_w2);
          auto.

        clear H_aux.
        intro H_absj_b01.
        elim (Qgt_alt (absj_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b01).
        clear H_aux1 H_aux2.
        intro H_absj_b01_eq_cmp.
        elim (Qeq_alt (absj_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b02).
        clear H_aux1 H_aux2.
        intro H_absj_b02_eq_cmp.
        simpl.
        rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.

        assert (H_a1_0_eq_absj_w1: in_abstractionj w1 a1_0).
          assert (H_a1_in_a1_0: absj_included_test a1 a1_0).
            apply absj_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_absj_w1).

        assert (H_absj_b02_le_0: absj_b0 a2 <= 0).
          rewrite H_absj_b02.
          apply Qle_refl.
        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1_0 H_absj_b01_0
            H_wf_a2 H_absj_b02_le_0
            H_a1_0_eq_absj_w1 H_a2_eq_absj_w2
            i H_on).
        decompose [and] H_a1_0.
        rewrite H2, H1.
        rewrite ones_pred_i_eq_ones_i; auto.

        intros H_aux H_absj_b01.
        elim H_aux.
        clear H_aux.
        intro H_absj_b02.
        elim (Qeq_alt (absj_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b01).
        clear H_aux1 H_aux2.
        intro H_absj_b01_eq_cmp.
        elim (Qlt_alt (absj_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b02).
        clear H_aux1 H_aux2.
        intro H_absj_b02_eq_cmp.
        simpl.
        rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.
        assert (H_absj_b01_le_0: absj_b0 a1 <= 0).
          rewrite H_absj_b01.
          apply Qle_refl.
        rewrite ones_pred_i_eq_ones_i; auto.
        apply
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 H_absj_b01_le_0
            H_wf_a2 (Qlt_le_weak (absj_b0 a2) 0 H_absj_b02)
            H_a1_eq_absj_w1 H_a2_eq_absj_w2);
          auto.

        clear H_aux.
        intro H_absj_b02.
        elim (Qeq_alt (absj_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b01).
        clear H_aux1 H_aux2.
        intro H_absj_b01_eq_cmp.
        elim (Qgt_alt (absj_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b02).
        clear H_aux1 H_aux2.
        intro H_absj_b02_eq_cmp.
        simpl.
        rewrite H_absj_b01_eq_cmp.
        rewrite H_absj_b02_eq_cmp.

        assert (H_a2_0_eq_absj_w2: in_abstractionj w2 a2_0).
          assert (H_a2_in_a2_0: absj_included_test a2 a2_0).
            apply absj_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_absj_w2).

        assert (H_absj_b01_le_0: absj_b0 a1 <= 0).
          rewrite H_absj_b01.
          apply Qle_refl.
        generalize
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 H_absj_b01_le_0
            H_wf_a2_0 H_absj_b02_0
            H_a1_eq_absj_w1 H_a2_0_eq_absj_w2
            i H_on).
        decompose [and] H_a2_0.
        rewrite H2, H1.
        rewrite ones_pred_i_eq_ones_i; auto.

        intros H_absj_b02 H_absj_b01.
        elim (Qeq_alt (absj_b0 a1) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b01).
        clear H_aux1 H_aux2.
        intro H_absj_b01_eq_cmp.
        elim (Qeq_alt (absj_b0 a2) 0).
        intros H_aux1 H_aux2.
        generalize (H_aux1 H_absj_b02).
        clear H_aux1 H_aux2.
        intro H_absj_b02_eq_cmp.
        simpl.
        rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.

        assert (H_absj_b01_le_0: absj_b0 a1 <= 0).
          rewrite H_absj_b01.
          apply Qle_refl.
        assert (H_absj_b02_le_0: absj_b0 a2 <= 0).
          rewrite H_absj_b02.
          apply Qle_refl.
        rewrite ones_pred_i_eq_ones_i; auto.
        apply
          (on_w1_w2_ge_on_a1_a2
            H_wf_a1 H_absj_b01_le_0
            H_wf_a2 H_absj_b02_le_0
            H_a1_eq_absj_w1 H_a2_eq_absj_w2
            i H_on).
  Qed.

  Property on_absj_correctness_aux:
    forall (w1:ibw) (w2:ibw),
    forall (a1:abstractionj) (a2:abstractionj),
    forall H_wf_a1: well_formed_abstractionj a1,
    forall H_wf_a2: well_formed_abstractionj a2,
    forall H_a1_eq_absj_w1: in_abstractionj w1 a1,
    forall H_a2_eq_absj_w2: in_abstractionj w2 a2,
    in_abstractionj (on w1 w2) (on_absj a1 a2).
  Proof.
    intros.
    unfold on_absj.
    apply on_absj_alt_correctness_aux; auto;
      try solve [
        apply absj_std_well_formed_abstractionj_compat; auto];
      try solve [
        apply absj_std_in_abstractionj_compat; auto].
      rewrite absj_std_red.
      simpl.
      rewrite Pmult_comm.
      reflexivity.
      rewrite absj_std_red.
      simpl.
      rewrite Pmult_comm.
      reflexivity.
  Qed.

  Property on_absj_alt_well_formed_abstractionj_compat:
    forall a1 a2: abstractionj,
    forall H_wf1: well_formed_abstractionj a1,
    forall H_wf2: well_formed_abstractionj a2,
    well_formed_abstractionj (on_absj_alt a1 a2).
  Proof.
    intros.
    unfold well_formed_abstractionj.
    simpl.
    destruct H_wf1 as [Ha1_0 Ha1_1].
    destruct H_wf2 as [Ha2_0 Ha2_1].
    split.
      apply Qmult_le_0_compat; assumption.

      apply (Qle_trans
        (absj_r a1 * absj_r a2)
        (1 * absj_r a2)
        1); try solve [ ring_simplify; auto ].
      apply Qmult_le_compat_r; auto.
  Qed.

End on_properties.


Section not_properties.

  Property not_absj_correctness_aux:
    forall w: ibw,

    forall a:abstractionj,
    forall H_wf_a: well_formed_abstractionj a,
    forall H_a_eq_absj_w: in_abstractionj w a,
    forall H_wf_b1: Qden (absj_b1 a) = Qden (absj_r a),
    in_abstractionj (not w) (not_absj a).
  Proof.
    intros.
    unfold in_abstractionj.
    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.
      rewrite ones_not_def.
      assert (H_aux: (i' - ones w i')%nat == i' - ones w i').
        apply minus_impl_Qminus.
        apply ones_i_le_i.
      rewrite H_aux; clear H_aux.
      pose (H_tmp:= H_a_eq_absj_w (S i') H_i_ge_1).
      elim H_tmp; clear H_tmp.
      intros H_true H_false.
      simpl in H_true, H_false.
      split.
        intro H_not_w.
        simpl.
        assert (H_w: w (S i') = false).
          case_eq (w (S i')); auto.
          intro H_w.
          simpl in H_not_w.
          rewrite H_w in H_not_w.
          simpl in H_not_w; congruence.
        pose (H_cc:= H_false H_w).
        apply <- Qlt_minus_iff.
        rewrite <- n_plus_1_eq_S_n.
        assert (H_aux:
          (1 - absj_r a) * (i' + 1) + (- absj_b0 a - (1 - (1 # Qden (absj_r a)))) + - (i' - ones w i') ==
          ones w i' + (1 # Qden (absj_r a)) + - (absj_r a * (i' + 1) + absj_b0 a)).
          ring.
        rewrite H_aux; clear H_aux.
        apply -> Qlt_minus_iff.
        rewrite n_plus_1_eq_S_n.
        apply Qle_impl_Qlt; try solve [ exact H_cc ].
        compute; reflexivity.

        intro H_not_w.
        simpl.
        assert (H_w: w (S i') = true).
          case_eq (w (S i')); auto.
          intro H_w.
          simpl in H_not_w.
          rewrite H_w in H_not_w.
          simpl in H_not_w; congruence.
        pose (H_cc:= H_true H_w).
        apply <- Qle_minus_iff.
        rewrite <- n_plus_1_eq_S_n.
        assert (H_aux:
          i' - ones w i' +
          - ((1 - absj_r a) * (i' + 1) + (- absj_b1 a - (1 - (1 # Qden (absj_r a)))))
          ==
          absj_r a * (i' + 1) + absj_b1 a - (1 # Qden (absj_r a)) - ones w i').
          ring.
        rewrite H_aux; clear H_aux.
        apply -> Qle_minus_iff.
        rewrite n_plus_1_eq_S_n.
        rewrite <- (Qred_correct (absj_r a * S i' + absj_b1 a)).
        apply Qlt_impl_Qle_red; auto.
        apply den_r_le_den_r_i_p_b; auto.
  Qed.

  Lemma absj_included_test_not_not_absj:
    forall a: abstractionj,
    absj_included_test a (not_absj (not_absj a)).
  Proof.
    intros.
    unfold absj_included_test.
    repeat split.
      simpl.
      ring.

      simpl.
      ring_simplify.
      apply Qle_refl.

      simpl.
      ring_simplify.
      apply Qle_refl.
  Qed.

  Lemma not_not_absj_included_test_absj:
    forall a: abstractionj,
    absj_included_test (not_absj (not_absj a)) a.
  Proof.
    intros.
    unfold absj_included_test.
    repeat split.
      simpl.
      ring.

      simpl.
      ring_simplify.
      apply Qle_refl.

      simpl.
      ring_simplify.
      apply Qle_refl.
  Qed.

  Property not_not_absj_equal_absj:
    forall a: abstractionj,
    absj_equal (not_absj (not_absj a)) a.
  Proof.
    intros.
    apply absj_equiv_test_impl_absj_equal.
    split.
      apply not_not_absj_included_test_absj.
      apply absj_included_test_not_not_absj.
  Qed.

  Property not_std_correctness:
    forall w: ibw,
    forall a:abstractionj,
    forall H_wf_a: well_formed_abstractionj a,
    forall H_a_eq_absj_w: in_abstractionj w a,
    in_abstractionj (not w) (not_absj (absj_std a)).
  Proof.
    intros.
    assert (H_wf_std_a: well_formed_abstractionj (absj_std a)).
      unfold well_formed_abstractionj.
      rewrite absj_std_red.
      simpl.
      assert (H_aux: (QDen (absj_b1 a) # Qden (absj_b1 a)) == 1).
        unfold Qeq.
        simpl.
        rewrite Pmult_1_r.
        reflexivity.
      rewrite H_aux; clear H_aux.
      rewrite Qmult_1_r.
      assumption.

    apply not_absj_correctness_aux; auto.
      apply (absj_equal_correctness H_wf_a H_wf_std_a); auto.
      apply absj_std_correctness.

      simpl.
      apply Pmult_comm.
  Qed.

  Property not_absj_well_formed_abstractionj_compat:
    forall a: abstractionj,
    forall H_wf: well_formed_abstractionj a,
    well_formed_abstractionj (not_absj a).
  Proof.
    intros.
    unfold well_formed_abstractionj.
    simpl.
    destruct H_wf as [H0 H1].
    split.
      apply -> Qle_minus_iff.
      assumption.

      apply <- Qle_minus_iff.
      ring_simplify.
      assumption.
  Qed.

  Property pre_not_absj_std_well_formed_abstractionj_compat:
    forall a: abstractionj,
    forall H_wf: well_formed_abstractionj a,
    well_formed_abstractionj (absj_std a).
  Proof.
    intros.
    unfold well_formed_abstractionj.
    rewrite absj_std_red.
    simpl.
    assert (H_aux: (QDen (absj_b1 a) # Qden (absj_b1 a)) == 1).
      unfold Qeq.
      simpl.
      rewrite Pmult_1_r.
      reflexivity.
    rewrite H_aux; clear H_aux.
    rewrite Qmult_1_r.
    assumption.
  Qed.

End not_properties.


Section prec_absj_properties.

  Property w_early_prec_a:
    forall a: abstractionj,
    forall H_wf: well_formed_abstractionj a,
    forall w: ibw,
    forall H_w_in_a: in_abstractionj 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: abstractionj,
    forall H_wf: well_formed_abstractionj a,
    forall w: ibw,
    forall H_w_in_a: in_abstractionj 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_absj_alt_correctness:
    forall a1 a2: abstractionj,
    forall H_wf1: well_formed_abstractionj a1,
    forall H_wf2: well_formed_abstractionj a2,
    forall H_prec_test: prec_absj_alt a1 a2,
    prec_absj a1 a2.
  Proof.
    intros.
    unfold prec_absj.
    intros.
    pose (H_early2_prec_w2:= w_early_prec_a H_wf2 H_w2_in_a2).
    unfold prec_absj_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_absj_alt_complet:
    forall a1 a2: abstractionj,
    forall H_wf1: well_formed_abstractionj a1,
    forall H_non_empty1: non_empty a1,
    forall H_wf2: well_formed_abstractionj a2,
    forall H_non_empty2: non_empty a2,
    forall H_prec: prec_absj a1 a2,
    prec_absj_alt a1 a2.
  Proof.
    intros.
    unfold prec_absj_alt.
    unfold prec_absj in H_prec.
    apply H_prec.
    apply late_in_abs; auto.
    apply early_in_abs; auto.
  Qed.

  Property prec_absj_test_correctness_aux:
    forall a1 a2: abstractionj,
    forall H_wf1: well_formed_abstractionj a1,
    forall H_wf2: well_formed_abstractionj a2,
    forall H_prec_test: prec_absj_test a1 a2,
    forall H_sync: absj_r a1 == absj_r a2,
    prec_absj a1 a2.
  Proof.
    intros.
    apply prec_absj_alt_correctness; auto.
    unfold prec_absj_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 cg_monotone_linear.
    unfold prec_absj_test in H_prec_test.
    rewrite H_sync.
    apply Qplus_le_compat; try solve [ apply Qle_refl ].
    assumption.
  Qed.

End prec_absj_properties.