Destruct if condition in program fixpoint Coq

Link:: https://stackoverflow.com/q/51017689

Display all goals and responses

Question

I want to proof the factor function correctness in Use proof of if expression = true in then part coq

Require Import ZArith Znumtheory.

Local Open Scope Z_scope.

Require Coq.Program.Wf.
Require Import Coq.micromega.Lia.

Lemma divgt0 (a b : Z) (agt0 : 0 < a) (bgt1 : 1 < b) (dvd : (b | a)) :
  0 < a / b.a, b: Z
agt0: 0 < a
bgt1: 1 < b
dvd: (b | a)
0 < a / b
Proof.a, b: Z
agt0: 0 < a
bgt1: 1 < b
dvd: (b | a)
0 < a / b
  now apply Zdivide_Zdiv_lt_pos.
Qed.

Program Fixpoint factor (a b : Z) (agt0 : 0 < a) (bgt1 : 1 < b)
        {measure (Z.abs_nat a)} :=
  if Zdivide_dec b a
  then 1 + factor (a / b) b (divgt0 a b agt0 bgt1 _)  bgt1
  else 0.
Next Obligation.a, b: Z
agt0: 0 < a
bgt1: 1 < b
factor: forall a0 b : Z,
0 < a0 ->
1 < b ->
(Z.abs_nat a0 < Z.abs_nat a)%nat -> Z
H: (b | a)
(Z.abs_nat (a / b) < Z.abs_nat a)%nat
  assert (0 < a / b < a).a, b: Z
agt0: 0 < a
bgt1: 1 < b
factor: forall a0 b : Z,
0 < a0 ->
1 < b ->
(Z.abs_nat a0 < Z.abs_nat a)%nat -> Z
H: (b | a)
0 < a / b < a
a, b: Z
agt0: 0 < a
bgt1: 1 < b
factor: forall a0 b : Z,
0 < a0 ->
1 < b ->
(Z.abs_nat a0 < Z.abs_nat a)%nat -> Z
H: (b | a)
H0: 0 < a / b < a
(Z.abs_nat (a / b) < Z.abs_nat a)%nat
  -a, b: Z
agt0: 0 < a
bgt1: 1 < b
factor: forall a0 b : Z,
0 < a0 ->
1 < b ->
(Z.abs_nat a0 < Z.abs_nat a)%nat -> Z
H: (b | a)
0 < a / b < a now apply Zdivide_Zdiv_lt_pos.
  -a, b: Z
agt0: 0 < a
bgt1: 1 < b
factor: forall a0 b : Z,
0 < a0 ->
1 < b ->
(Z.abs_nat a0 < Z.abs_nat a)%nat -> Z
H: (b | a)
H0: 0 < a / b < a
(Z.abs_nat (a / b) < Z.abs_nat a)%nat apply Zabs_nat_lt.a, b: Z
agt0: 0 < a
bgt1: 1 < b
factor: forall a0 b : Z,
0 < a0 ->
1 < b ->
(Z.abs_nat a0 < Z.abs_nat a)%nat -> Z
H: (b | a)
H0: 0 < a / b < a
0 <= a / b < a lia.
Qed.

Lemma factor_div (a b : Z) (agt0 : 0 < a) (bgt1 : 1 < b) :
  (b ^ (factor a b agt0 bgt1) | a).a, b: Z
agt0: 0 < a
bgt1: 1 < b
(b ^ factor a b agt0 bgt1 | a)
Proof.a, b: Z
agt0: 0 < a
bgt1: 1 < b
(b ^ factor a b agt0 bgt1 | a)
  unfold factor.a, b: Z
agt0: 0 < a
bgt1: 1 < b
(b
 ^ factor_func
     (existT
        (fun a : Z =>
         {b : Z | exists _ : 0 < a, 1 < b}) a
        (exist (fun b : Z => exists _ : 0 < a, 1 < b)
           b
           (ex_intro (fun _ : 0 < a => 1 < b) agt0
              bgt1))) | a)

after unfold I expected see a if and destruct its condition, but now I see this:

1 subgoal

  a, b : Z
  agt0 : 0 < a
  bgt1 : 1 < b
  ============================
  (b
   ^ factor_func
       (existT
          (fun a0 : Z =>
           {b0 : Z | exists _ : 0 < a0, 1 < b0}) a
          (exist
             (fun b0 : Z => exists _ : 0 < a, 1 < b0)
             b
             (ex_intro (fun _ : 0 < a => 1 < b) agt0
                bgt1))) | a)

How I can complete the proof?

Answer

Program gives you terms that are difficult to work with, so you should prove a lemma that factor is equal to its body, and then rewrite with that, instead of unfolding. (I used match instead of if to get hold of the dvd proof term.)

Lemma factor_lemma a b agt0 bgt1:
  factor a b agt0 bgt1 =
  match Zdivide_dec b a with
  | left dvd => 1 + factor (a / b) b (divgt0 a b agt0 bgt1 dvd) bgt1
  | right notdvd => 0
  end.a, b: Z
agt0: 0 < a
bgt1: 1 < b
factor a b agt0 bgt1 =
match Zdivide_dec b a with
| left dvd =>
    1 +
    factor (a / b) b (divgt0 a b agt0 bgt1 dvd) bgt1
| right _ => 0
end
Proof.a, b: Z
agt0: 0 < a
bgt1: 1 < b
factor a b agt0 bgt1 =
match Zdivide_dec b a with
| left dvd =>
    1 +
    factor (a / b) b (divgt0 a b agt0 bgt1 dvd) bgt1
| right _ => 0
end
  unfold factor at 1.a, b: Z
agt0: 0 < a
bgt1: 1 < b
factor_func
  (existT
     (fun a : Z => {b : Z | exists _ : 0 < a, 1 < b})
     a
     (exist (fun b : Z => exists _ : 0 < a, 1 < b) b
        (ex_intro (fun _ : 0 < a => 1 < b) agt0 bgt1))) =
match Zdivide_dec b a with
| left dvd =>
    1 +
    factor (a / b) b (divgt0 a b agt0 bgt1 dvd) bgt1
| right _ => 0
end unfold factor_func.a, b: Z
agt0: 0 < a
bgt1: 1 < b
Wf.Fix_sub {a : Z & {b : Z | exists _ : 0 < a, 1 < b}}
  (Wf.MR lt
     (fun
        recarg : {a : Z &
                 {b : Z | exists _ : 0 < a, 1 < b}} =>
      Z.abs_nat (projT1 recarg)))
  factor_func_obligation_3
  (fun _ : {a : Z & {b : Z | exists _ : 0 < a, 1 < b}}
   => Z)
  (fun
     (recarg : {a : Z &
               {b : Z | exists _ : 0 < a, 1 < b}})
     (factor' : {recarg'
                : {a : Z &
                  {b : Z | exists _ : 0 < a, 1 < b}}
                | (Z.abs_nat (projT1 recarg') <
                   Z.abs_nat (projT1 recarg))%nat} ->
                Z) =>
   match
     Zdivide_dec (proj1_sig (projT2 recarg))
       (projT1 recarg)
   with
   | left x =>
       1 +
       factor'
         (exist
            (fun
               recarg' : 
                {a : Z &
                {b : Z | exists _ : 0 < a, 1 < b}} =>
             (Z.abs_nat (projT1 recarg') <
              Z.abs_nat (projT1 recarg))%nat)
            (existT
               (fun a : Z =>
                {b : Z | exists _ : 0 < a, 1 < b})
               (projT1 recarg /
                proj1_sig (projT2 recarg))
               (exist
                  (fun b : Z =>
                   exists
                     _ : 
                      0 <
                      projT1 recarg /
                      proj1_sig (projT2 recarg), 
                   1 < b) 
                  (proj1_sig (projT2 recarg))
                  (ex_intro
                     (fun
                        _ : 
                        0 <
                        projT1 recarg /
                        proj1_sig (projT2 recarg) =>
                      1 < proj1_sig (projT2 recarg))
                     (divgt0 
                        (projT1 recarg)
                        (proj1_sig (projT2 recarg))
                        (ex_proj1
                        (proj2_sig (projT2 recarg)))
                        (ex_proj2
                        (proj2_sig (projT2 recarg)))
                        (factor_func_obligation_1
                        (projT1 recarg)
                        (proj1_sig (projT2 recarg)) x))
                     (ex_proj2
                        (proj2_sig (projT2 recarg))))))
            (factor_func_obligation_2 
               (projT1 recarg)
               (proj1_sig (projT2 recarg))
               (ex_proj1 (proj2_sig (projT2 recarg)))
               (ex_proj2 (proj2_sig (projT2 recarg)))
               x))
   | right _ => 0
   end)
  (existT
     (fun a : Z => {b : Z | exists _ : 0 < a, 1 < b})
     a
     (exist (fun b : Z => exists _ : 0 < a, 1 < b) b
        (ex_intro (fun _ : 0 < a => 1 < b) agt0 bgt1))) =
match Zdivide_dec b a with
| left dvd =>
    1 +
    factor (a / b) b (divgt0 a b agt0 bgt1 dvd) bgt1
| right _ => 0
end
  rewrite Program.Wf.Fix_eq; fold factor_func.a, b: Z
agt0: 0 < a
bgt1: 1 < b
match
  Zdivide_dec
    (proj1_sig
       (projT2
          (existT
             (fun a : Z =>
              {b : Z | exists _ : 0 < a, 1 < b}) a
             (exist
                (fun b : Z => exists _ : 0 < a, 1 < b)
                b
                (ex_intro 
                   (fun _ : 0 < a => 1 < b) agt0 bgt1)))))
    (projT1
       (existT
          (fun a : Z =>
           {b : Z | exists _ : 0 < a, 1 < b}) a
          (exist
             (fun b : Z => exists _ : 0 < a, 1 < b) b
             (ex_intro (fun _ : 0 < a => 1 < b) agt0
                bgt1))))
with
| left x =>
    1 +
    factor_func
      (proj1_sig
         (exist
            (fun
               recarg' : 
                {a : Z &
                {b : Z | exists _ : 0 < a, 1 < b}} =>
             (Z.abs_nat (projT1 recarg') <
              Z.abs_nat
                (projT1
                   (existT
                      (fun a : Z =>
                       {b : Z
                       | 
                       exists 
                       _ : (0 < a)%Z, 
                       (1 < b)%Z}) a
                      (exist
                        (fun b : Z =>
                        exists 
                        _ : (0 < a)%Z, 
                        (1 < b)%Z) b
                        (ex_intro
                        (fun _ : (...)%Z => (1 < b)%Z)
                        agt0 bgt1)))))%nat)
            (existT
               (fun a : Z =>
                {b : Z | exists _ : 0 < a, 1 < b})
               (projT1
                  (existT
                     (fun a : Z =>
                      {b : Z
                      | exists _ : 0 < a, 1 < b}) a
                     (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : 0 < a => 1 < b) agt0
                        bgt1))) /
                proj1_sig
                  (projT2
                     (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : 0 < a, 1 < b}) a
                        (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : 0 < a => 1 < b) agt0
                        bgt1)))))
               (exist
                  (fun b0 : Z =>
                   exists
                     _ : 
                      0 <
                      projT1
                        (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : ..., 1 < b}) a
                        (exist
                        (fun ... => exists ..., ...) b
                        (ex_intro (...) agt0 bgt1))) /
                      proj1_sig
                        (projT2
                        (existT
                        (fun ... => {b : Z | ...}) a
                        (exist (...) b (...)))),
                     1 < b0)
                  (proj1_sig
                     (projT2
                        (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : 0 < a, 1 < b}) a
                        (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : ... => 1 < b) agt0
                        bgt1)))))
                  (ex_intro
                     (fun
                        _ : 
                        0 <
                        projT1
                        (existT
                        (fun ... => {b : Z | ...}) a
                        (exist (...) b (...))) /
                        proj1_sig
                        (projT2 (existT (...) a (...)))
                      =>
                      1 <
                      proj1_sig
                        (projT2
                        (existT
                        (fun a : Z =>
                        {b : Z | exists ..., ...}) a
                        (exist 
                        (... => ...) b
                        (ex_intro ... agt0 bgt1)))))
                     (divgt0
                        (projT1
                        (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : 0 < a, 1 < b}) a
                        (exist
                        (fun b : Z =>
                        exists _ : ..., 1 < b) b
                        (ex_intro 
                        (... => ...) agt0 bgt1))))
                        (proj1_sig
                        (projT2
                        (existT
                        (fun a : Z =>
                        {b : Z | exists ..., ...}) a
                        (exist 
                        (... => ...) b
                        (ex_intro ... agt0 bgt1)))))
                        (ex_proj1
                        (proj2_sig
                        (projT2
                        (existT 
                        (... => ...) a
                        (exist ... b ...)))))
                        (ex_proj2
                        (proj2_sig
                        (projT2
                        (existT 
                        (... => ...) a
                        (exist ... b ...)))))
                        (factor_func_obligation_1
                        (projT1
                        (existT
                        (fun a : Z =>
                        {b : Z | exists ..., ...}) a
                        (exist 
                        (... => ...) b
                        (ex_intro ... agt0 bgt1))))
                        (proj1_sig
                        (projT2
                        (existT 
                        (... => ...) a
                        (exist ... b ...)))) x))
                     (ex_proj2
                        (proj2_sig
                        (projT2
                        (existT
                        (fun a : Z =>
                        {b : Z | exists ..., ...}) a
                        (exist 
                        (... => ...) b
                        (ex_intro ... agt0 bgt1)))))))))
            (factor_func_obligation_2
               (projT1
                  (existT
                     (fun a : Z =>
                      {b : Z
                      | exists _ : 0 < a, 1 < b}) a
                     (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : 0 < a => 1 < b) agt0
                        bgt1))))
               (proj1_sig
                  (projT2
                     (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : 0 < a, 1 < b}) a
                        (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : 0 < a => 1 < b) agt0
                        bgt1)))))
               (ex_proj1
                  (proj2_sig
                     (projT2
                        (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : 0 < a, 1 < b}) a
                        (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : ... => 1 < b) agt0
                        bgt1))))))
               (ex_proj2
                  (proj2_sig
                     (projT2
                        (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : 0 < a, 1 < b}) a
                        (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : ... => 1 < b) agt0
                        bgt1)))))) x)))
| right _ => 0
end =
match Zdivide_dec b a with
| left dvd =>
    1 +
    factor (a / b) b (divgt0 a b agt0 bgt1 dvd) bgt1
| right _ => 0
end
a, b: Z
agt0: 0 < a
bgt1: 1 < b
forall
  (x : {a : Z & {b : Z | exists _ : 0 < a, 1 < b}})
  (f
   g : {y
       : {a : Z & {b : Z | exists _ : 0 < a, 1 < b}}
       | Wf.MR lt
           (fun
              recarg : {a : Z &
                       {b : Z
                       | 
                       exists _ : 0 < a, 1 < b}} =>
            Z.abs_nat (projT1 recarg)) y x} -> Z),
(forall
   y : {y
       : {a : Z & {b : Z | exists _ : 0 < a, 1 < b}}
       | Wf.MR lt
           (fun
              recarg : {a : Z &
                       {b : Z
                       | 
                       exists _ : 0 < a, 1 < b}} =>
            Z.abs_nat (projT1 recarg)) y x}, 
 f y = g y) ->
match
  Zdivide_dec (proj1_sig (projT2 x)) (projT1 x)
with
| left x0 =>
    1 +
    f
      (exist
         (fun
            recarg' : {a : Z &
                      {b : Z
                      | exists _ : 0 < a, 1 < b}} =>
          (Z.abs_nat (projT1 recarg') <
           Z.abs_nat (projT1 x))%nat)
         (existT
            (fun a : Z =>
             {b : Z | exists _ : 0 < a, 1 < b})
            (projT1 x / proj1_sig (projT2 x))
            (exist
               (fun b : Z =>
                exists
                  _ : 0 <
                      projT1 x / proj1_sig (projT2 x),
                  1 < b) 
               (proj1_sig (projT2 x))
               (ex_intro
                  (fun
                     _ : 
                      0 <
                      projT1 x / proj1_sig (projT2 x)
                   => 1 < proj1_sig (projT2 x))
                  (divgt0 
                     (projT1 x) 
                     (proj1_sig (projT2 x))
                     (ex_proj1 (proj2_sig (projT2 x)))
                     (ex_proj2 (proj2_sig (projT2 x)))
                     (factor_func_obligation_1
                        (projT1 x)
                        (proj1_sig (projT2 x)) x0))
                  (ex_proj2 (proj2_sig (projT2 x))))))
         (factor_func_obligation_2 
            (projT1 x) (proj1_sig (projT2 x))
            (ex_proj1 (proj2_sig (projT2 x)))
            (ex_proj2 (proj2_sig (projT2 x))) x0))
| right _ => 0
end =
match
  Zdivide_dec (proj1_sig (projT2 x)) (projT1 x)
with
| left x0 =>
    1 +
    g
      (exist
         (fun
            recarg' : {a : Z &
                      {b : Z
                      | exists _ : 0 < a, 1 < b}} =>
          (Z.abs_nat (projT1 recarg') <
           Z.abs_nat (projT1 x))%nat)
         (existT
            (fun a : Z =>
             {b : Z | exists _ : 0 < a, 1 < b})
            (projT1 x / proj1_sig (projT2 x))
            (exist
               (fun b : Z =>
                exists
                  _ : 0 <
                      projT1 x / proj1_sig (projT2 x),
                  1 < b) 
               (proj1_sig (projT2 x))
               (ex_intro
                  (fun
                     _ : 
                      0 <
                      projT1 x / proj1_sig (projT2 x)
                   => 1 < proj1_sig (projT2 x))
                  (divgt0 
                     (projT1 x) 
                     (proj1_sig (projT2 x))
                     (ex_proj1 (proj2_sig (projT2 x)))
                     (ex_proj2 (proj2_sig (projT2 x)))
                     (factor_func_obligation_1
                        (projT1 x)
                        (proj1_sig (projT2 x)) x0))
                  (ex_proj2 (proj2_sig (projT2 x))))))
         (factor_func_obligation_2 
            (projT1 x) (proj1_sig (projT2 x))
            (ex_proj1 (proj2_sig (projT2 x)))
            (ex_proj2 (proj2_sig (projT2 x))) x0))
| right _ => 0
end
  -a, b: Z
agt0: 0 < a
bgt1: 1 < b
match
  Zdivide_dec
    (proj1_sig
       (projT2
          (existT
             (fun a : Z =>
              {b : Z | exists _ : 0 < a, 1 < b}) a
             (exist
                (fun b : Z => exists _ : 0 < a, 1 < b)
                b
                (ex_intro 
                   (fun _ : 0 < a => 1 < b) agt0 bgt1)))))
    (projT1
       (existT
          (fun a : Z =>
           {b : Z | exists _ : 0 < a, 1 < b}) a
          (exist
             (fun b : Z => exists _ : 0 < a, 1 < b) b
             (ex_intro (fun _ : 0 < a => 1 < b) agt0
                bgt1))))
with
| left x =>
    1 +
    factor_func
      (proj1_sig
         (exist
            (fun
               recarg' : 
                {a : Z &
                {b : Z | exists _ : 0 < a, 1 < b}} =>
             (Z.abs_nat (projT1 recarg') <
              Z.abs_nat
                (projT1
                   (existT
                      (fun a : Z =>
                       {b : Z
                       | 
                       exists 
                       _ : (0 < a)%Z, 
                       (1 < b)%Z}) a
                      (exist
                        (fun b : Z =>
                        exists 
                        _ : (0 < a)%Z, 
                        (1 < b)%Z) b
                        (ex_intro
                        (fun _ : (...)%Z => (1 < b)%Z)
                        agt0 bgt1)))))%nat)
            (existT
               (fun a : Z =>
                {b : Z | exists _ : 0 < a, 1 < b})
               (projT1
                  (existT
                     (fun a : Z =>
                      {b : Z
                      | exists _ : 0 < a, 1 < b}) a
                     (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : 0 < a => 1 < b) agt0
                        bgt1))) /
                proj1_sig
                  (projT2
                     (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : 0 < a, 1 < b}) a
                        (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : 0 < a => 1 < b) agt0
                        bgt1)))))
               (exist
                  (fun b0 : Z =>
                   exists
                     _ : 
                      0 <
                      projT1
                        (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : ..., 1 < b}) a
                        (exist
                        (fun ... => exists ..., ...) b
                        (ex_intro (...) agt0 bgt1))) /
                      proj1_sig
                        (projT2
                        (existT
                        (fun ... => {b : Z | ...}) a
                        (exist (...) b (...)))),
                     1 < b0)
                  (proj1_sig
                     (projT2
                        (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : 0 < a, 1 < b}) a
                        (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : ... => 1 < b) agt0
                        bgt1)))))
                  (ex_intro
                     (fun
                        _ : 
                        0 <
                        projT1
                        (existT
                        (fun ... => {b : Z | ...}) a
                        (exist (...) b (...))) /
                        proj1_sig
                        (projT2 (existT (...) a (...)))
                      =>
                      1 <
                      proj1_sig
                        (projT2
                        (existT
                        (fun a : Z =>
                        {b : Z | exists ..., ...}) a
                        (exist 
                        (... => ...) b
                        (ex_intro ... agt0 bgt1)))))
                     (divgt0
                        (projT1
                        (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : 0 < a, 1 < b}) a
                        (exist
                        (fun b : Z =>
                        exists _ : ..., 1 < b) b
                        (ex_intro 
                        (... => ...) agt0 bgt1))))
                        (proj1_sig
                        (projT2
                        (existT
                        (fun a : Z =>
                        {b : Z | exists ..., ...}) a
                        (exist 
                        (... => ...) b
                        (ex_intro ... agt0 bgt1)))))
                        (ex_proj1
                        (proj2_sig
                        (projT2
                        (existT 
                        (... => ...) a
                        (exist ... b ...)))))
                        (ex_proj2
                        (proj2_sig
                        (projT2
                        (existT 
                        (... => ...) a
                        (exist ... b ...)))))
                        (factor_func_obligation_1
                        (projT1
                        (existT
                        (fun a : Z =>
                        {b : Z | exists ..., ...}) a
                        (exist 
                        (... => ...) b
                        (ex_intro ... agt0 bgt1))))
                        (proj1_sig
                        (projT2
                        (existT 
                        (... => ...) a
                        (exist ... b ...)))) x))
                     (ex_proj2
                        (proj2_sig
                        (projT2
                        (existT
                        (fun a : Z =>
                        {b : Z | exists ..., ...}) a
                        (exist 
                        (... => ...) b
                        (ex_intro ... agt0 bgt1)))))))))
            (factor_func_obligation_2
               (projT1
                  (existT
                     (fun a : Z =>
                      {b : Z
                      | exists _ : 0 < a, 1 < b}) a
                     (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : 0 < a => 1 < b) agt0
                        bgt1))))
               (proj1_sig
                  (projT2
                     (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : 0 < a, 1 < b}) a
                        (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : 0 < a => 1 < b) agt0
                        bgt1)))))
               (ex_proj1
                  (proj2_sig
                     (projT2
                        (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : 0 < a, 1 < b}) a
                        (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : ... => 1 < b) agt0
                        bgt1))))))
               (ex_proj2
                  (proj2_sig
                     (projT2
                        (existT
                        (fun a : Z =>
                        {b : Z
                        | 
                        exists _ : 0 < a, 1 < b}) a
                        (exist
                        (fun b : Z =>
                        exists _ : 0 < a, 1 < b) b
                        (ex_intro
                        (fun _ : ... => 1 < b) agt0
                        bgt1)))))) x)))
| right _ => 0
end =
match Zdivide_dec b a with
| left dvd =>
    1 +
    factor (a / b) b (divgt0 a b agt0 bgt1 dvd) bgt1
| right _ => 0
end reflexivity.
  -a, b: Z
agt0: 0 < a
bgt1: 1 < b
forall
  (x : {a : Z & {b : Z | exists _ : 0 < a, 1 < b}})
  (f
   g : {y
       : {a : Z & {b : Z | exists _ : 0 < a, 1 < b}}
       | Wf.MR lt
           (fun
              recarg : {a : Z &
                       {b : Z
                       | 
                       exists _ : 0 < a, 1 < b}} =>
            Z.abs_nat (projT1 recarg)) y x} -> Z),
(forall
   y : {y
       : {a : Z & {b : Z | exists _ : 0 < a, 1 < b}}
       | Wf.MR lt
           (fun
              recarg : {a : Z &
                       {b : Z
                       | 
                       exists _ : 0 < a, 1 < b}} =>
            Z.abs_nat (projT1 recarg)) y x}, 
 f y = g y) ->
match
  Zdivide_dec (proj1_sig (projT2 x)) (projT1 x)
with
| left x0 =>
    1 +
    f
      (exist
         (fun
            recarg' : {a : Z &
                      {b : Z
                      | exists _ : 0 < a, 1 < b}} =>
          (Z.abs_nat (projT1 recarg') <
           Z.abs_nat (projT1 x))%nat)
         (existT
            (fun a : Z =>
             {b : Z | exists _ : 0 < a, 1 < b})
            (projT1 x / proj1_sig (projT2 x))
            (exist
               (fun b : Z =>
                exists
                  _ : 0 <
                      projT1 x / proj1_sig (projT2 x),
                  1 < b) 
               (proj1_sig (projT2 x))
               (ex_intro
                  (fun
                     _ : 
                      0 <
                      projT1 x / proj1_sig (projT2 x)
                   => 1 < proj1_sig (projT2 x))
                  (divgt0 
                     (projT1 x) 
                     (proj1_sig (projT2 x))
                     (ex_proj1 (proj2_sig (projT2 x)))
                     (ex_proj2 (proj2_sig (projT2 x)))
                     (factor_func_obligation_1
                        (projT1 x)
                        (proj1_sig (projT2 x)) x0))
                  (ex_proj2 (proj2_sig (projT2 x))))))
         (factor_func_obligation_2 
            (projT1 x) (proj1_sig (projT2 x))
            (ex_proj1 (proj2_sig (projT2 x)))
            (ex_proj2 (proj2_sig (projT2 x))) x0))
| right _ => 0
end =
match
  Zdivide_dec (proj1_sig (projT2 x)) (projT1 x)
with
| left x0 =>
    1 +
    g
      (exist
         (fun
            recarg' : {a : Z &
                      {b : Z
                      | exists _ : 0 < a, 1 < b}} =>
          (Z.abs_nat (projT1 recarg') <
           Z.abs_nat (projT1 x))%nat)
         (existT
            (fun a : Z =>
             {b : Z | exists _ : 0 < a, 1 < b})
            (projT1 x / proj1_sig (projT2 x))
            (exist
               (fun b : Z =>
                exists
                  _ : 0 <
                      projT1 x / proj1_sig (projT2 x),
                  1 < b) 
               (proj1_sig (projT2 x))
               (ex_intro
                  (fun
                     _ : 
                      0 <
                      projT1 x / proj1_sig (projT2 x)
                   => 1 < proj1_sig (projT2 x))
                  (divgt0 
                     (projT1 x) 
                     (proj1_sig (projT2 x))
                     (ex_proj1 (proj2_sig (projT2 x)))
                     (ex_proj2 (proj2_sig (projT2 x)))
                     (factor_func_obligation_1
                        (projT1 x)
                        (proj1_sig (projT2 x)) x0))
                  (ex_proj2 (proj2_sig (projT2 x))))))
         (factor_func_obligation_2 
            (projT1 x) (proj1_sig (projT2 x))
            (ex_proj1 (proj2_sig (projT2 x)))
            (ex_proj2 (proj2_sig (projT2 x))) x0))
| right _ => 0
end intros.a, b: Z
agt0: 0 < a
bgt1: 1 < b
x: {a : Z & {b : Z | exists _ : 0 < a, 1 < b}}
f, g: {y : {a : Z & {b : Z | exists _ : 0 < a, 1 < b}}
| Wf.MR lt
    (fun
       recarg : {a : Z &
                {b : Z | exists _ : 0 < a, 1 < b}}
     => Z.abs_nat (projT1 recarg)) y x} -> Z
H: forall
  y : {y
      : {a : Z &
        {b : Z | exists _ : 0 < a, 1 < b}}
      | Wf.MR lt
          (fun
             recarg : {a : Z &
                      {b : Z
                      | exists _ : 0 < a, 1 < b}}
           => Z.abs_nat (projT1 recarg)) y x},
f y = g y
match
  Zdivide_dec (proj1_sig (projT2 x)) (projT1 x)
with
| left x0 =>
    1 +
    f
      (exist
         (fun
            recarg' : {a : Z &
                      {b : Z
                      | exists _ : 0 < a, 1 < b}} =>
          (Z.abs_nat (projT1 recarg') <
           Z.abs_nat (projT1 x))%nat)
         (existT
            (fun a : Z =>
             {b : Z | exists _ : 0 < a, 1 < b})
            (projT1 x / proj1_sig (projT2 x))
            (exist
               (fun b : Z =>
                exists
                  _ : 0 <
                      projT1 x / proj1_sig (projT2 x),
                  1 < b) 
               (proj1_sig (projT2 x))
               (ex_intro
                  (fun
                     _ : 
                      0 <
                      projT1 x / proj1_sig (projT2 x)
                   => 1 < proj1_sig (projT2 x))
                  (divgt0 
                     (projT1 x) 
                     (proj1_sig (projT2 x))
                     (ex_proj1 (proj2_sig (projT2 x)))
                     (ex_proj2 (proj2_sig (projT2 x)))
                     (factor_func_obligation_1
                        (projT1 x)
                        (proj1_sig (projT2 x)) x0))
                  (ex_proj2 (proj2_sig (projT2 x))))))
         (factor_func_obligation_2 
            (projT1 x) (proj1_sig (projT2 x))
            (ex_proj1 (proj2_sig (projT2 x)))
            (ex_proj2 (proj2_sig (projT2 x))) x0))
| right _ => 0
end =
match
  Zdivide_dec (proj1_sig (projT2 x)) (projT1 x)
with
| left x0 =>
    1 +
    g
      (exist
         (fun
            recarg' : {a : Z &
                      {b : Z
                      | exists _ : 0 < a, 1 < b}} =>
          (Z.abs_nat (projT1 recarg') <
           Z.abs_nat (projT1 x))%nat)
         (existT
            (fun a : Z =>
             {b : Z | exists _ : 0 < a, 1 < b})
            (projT1 x / proj1_sig (projT2 x))
            (exist
               (fun b : Z =>
                exists
                  _ : 0 <
                      projT1 x / proj1_sig (projT2 x),
                  1 < b) 
               (proj1_sig (projT2 x))
               (ex_intro
                  (fun
                     _ : 
                      0 <
                      projT1 x / proj1_sig (projT2 x)
                   => 1 < proj1_sig (projT2 x))
                  (divgt0 
                     (projT1 x) 
                     (proj1_sig (projT2 x))
                     (ex_proj1 (proj2_sig (projT2 x)))
                     (ex_proj2 (proj2_sig (projT2 x)))
                     (factor_func_obligation_1
                        (projT1 x)
                        (proj1_sig (projT2 x)) x0))
                  (ex_proj2 (proj2_sig (projT2 x))))))
         (factor_func_obligation_2 
            (projT1 x) (proj1_sig (projT2 x))
            (ex_proj1 (proj2_sig (projT2 x)))
            (ex_proj2 (proj2_sig (projT2 x))) x0))
| right _ => 0
end destruct Zdivide_dec; auto.a, b: Z
agt0: 0 < a
bgt1: 1 < b
x: {a : Z & {b : Z | exists _ : 0 < a, 1 < b}}
f, g: {y : {a : Z & {b : Z | exists _ : 0 < a, 1 < b}}
| Wf.MR lt
    (fun
       recarg : {a : Z &
                {b : Z | exists _ : 0 < a, 1 < b}}
     => Z.abs_nat (projT1 recarg)) y x} -> Z
H: forall
  y : {y
      : {a : Z &
        {b : Z | exists _ : 0 < a, 1 < b}}
      | Wf.MR lt
          (fun
             recarg : {a : Z &
                      {b : Z
                      | exists _ : 0 < a, 1 < b}}
           => Z.abs_nat (projT1 recarg)) y x},
f y = g y
d: (proj1_sig (projT2 x) | projT1 x)
1 +
f
  (exist
     (fun
        recarg' : {a : Z &
                  {b : Z | exists _ : 0 < a, 1 < b}}
      =>
      (Z.abs_nat (projT1 recarg') <
       Z.abs_nat (projT1 x))%nat)
     (existT
        (fun a : Z =>
         {b : Z | exists _ : 0 < a, 1 < b})
        (projT1 x / proj1_sig (projT2 x))
        (exist
           (fun b : Z =>
            exists
              _ : 0 < projT1 x / proj1_sig (projT2 x),
              1 < b) (proj1_sig (projT2 x))
           (ex_intro
              (fun
                 _ : 0 <
                     projT1 x / proj1_sig (projT2 x)
               => 1 < proj1_sig (projT2 x))
              (divgt0 (projT1 x)
                 (proj1_sig (projT2 x))
                 (ex_proj1 (proj2_sig (projT2 x)))
                 (ex_proj2 (proj2_sig (projT2 x)))
                 (factor_func_obligation_1 
                    (projT1 x) 
                    (proj1_sig (projT2 x)) d))
              (ex_proj2 (proj2_sig (projT2 x))))))
     (factor_func_obligation_2 
        (projT1 x) (proj1_sig (projT2 x))
        (ex_proj1 (proj2_sig (projT2 x)))
        (ex_proj2 (proj2_sig (projT2 x))) d)) =
1 +
g
  (exist
     (fun
        recarg' : {a : Z &
                  {b : Z | exists _ : 0 < a, 1 < b}}
      =>
      (Z.abs_nat (projT1 recarg') <
       Z.abs_nat (projT1 x))%nat)
     (existT
        (fun a : Z =>
         {b : Z | exists _ : 0 < a, 1 < b})
        (projT1 x / proj1_sig (projT2 x))
        (exist
           (fun b : Z =>
            exists
              _ : 0 < projT1 x / proj1_sig (projT2 x),
              1 < b) (proj1_sig (projT2 x))
           (ex_intro
              (fun
                 _ : 0 <
                     projT1 x / proj1_sig (projT2 x)
               => 1 < proj1_sig (projT2 x))
              (divgt0 (projT1 x)
                 (proj1_sig (projT2 x))
                 (ex_proj1 (proj2_sig (projT2 x)))
                 (ex_proj2 (proj2_sig (projT2 x)))
                 (factor_func_obligation_1 
                    (projT1 x) 
                    (proj1_sig (projT2 x)) d))
              (ex_proj2 (proj2_sig (projT2 x))))))
     (factor_func_obligation_2 
        (projT1 x) (proj1_sig (projT2 x))
        (ex_proj1 (proj2_sig (projT2 x)))
        (ex_proj2 (proj2_sig (projT2 x))) d)) congruence.
Qed.

When you unfold and rewrite with Fix_eq you get such a horrible goal term to look at that it's best to fold it quickly! :-) It can be handled with reflexivity or auto anyway.

The second goal typically requires algebraic manipulation with lia or similar to show that the LHS equals RHS, but in this case it was sufficient with congruence.

How did I know to use Fix_eq? When I unfolded factor_func I saw it contained Wf.Fix_sub, so I searched for lemmas with Search (Wf.Fix_sub). and found a few.

Now you should continue your proof by rewriting with the lemma:

Lemma factor_div (a b : Z) (agt0 : 0 < a) (bgt1 : 1 < b) :
  (b ^ (factor a b agt0 bgt1) | a).a, b: Z
agt0: 0 < a
bgt1: 1 < b
(b ^ factor a b agt0 bgt1 | a)
Proof.a, b: Z
agt0: 0 < a
bgt1: 1 < b
(b ^ factor a b agt0 bgt1 | a)
  rewrite factor_lemma.a, b: Z
agt0: 0 < a
bgt1: 1 < b
(b
 ^ match Zdivide_dec b a with
   | left dvd =>
       1 +
       factor (a / b) b (divgt0 a b agt0 bgt1 dvd)
         bgt1
   | right _ => 0
   end | a) destruct Zdivide_dec.a, b: Z
agt0: 0 < a
bgt1: 1 < b
d: (b | a)
(b
 ^ (1 + factor (a / b) b (divgt0 a b agt0 bgt1 d) bgt1)
| a)
a, b: Z
agt0: 0 < a
bgt1: 1 < b
n: ~ (b | a)
(b ^ 0 | a)
  2: now rewrite Z.pow_0_r; apply Z.divide_1_l.a, b: Z
agt0: 0 < a
bgt1: 1 < b
d: (b | a)
(b
 ^ (1 + factor (a / b) b (divgt0 a b agt0 bgt1 d) bgt1)
| a)

Now your goal state is

1 subgoal

  a, b : Z
  agt0 : 0 < a
  bgt1 : 1 < b
  d : (b | a)
  ============================
  (b
   ^ (1 +
      factor (a / b) b (divgt0 a b agt0 bgt1 d) bgt1)
  | a)

which probably makes more sense.