Apply nat_complete_ind to the current goal.
Let n be given.
Assume Hn: nat_p n.
Assume IH: ∀m ∈ n, 0 ∈ m → ∃k ∈ ω, ∃f : set → set, nonincrfinseq prime_nat k f ∧ Pi_SNo f k = m ∧ ∀k' ∈ ω, ∀f' : set → set, nonincrfinseq prime_nat k' f' → Pi_SNo f' k' = m → k' = k ∧ ∀i ∈ k, f' i = f i.
Assume H1: 0 ∈ n.
We prove the intermediate claim Ln: n ∈ ω.
An exact proof term for the current goal is nat_p_omega n Hn.
Apply xm (n = 1) to the current goal.
Assume H2: n = 1.
Set f to be the term λi ⇒ 0 of type set → set.
We will prove ∃k ∈ ω, ∃f : set → set, nonincrfinseq prime_nat k f ∧ Pi_SNo f k = n ∧ ∀k' ∈ ω, ∀f' : set → set, nonincrfinseq prime_nat k' f' → Pi_SNo f' k' = n → k' = k ∧ ∀i ∈ k, f' i = f i.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 0 ∈ ω.
An exact proof term for the current goal is nat_p_omega 0 nat_0.
We use f to witness the existential quantifier.
Apply and3I to the current goal.
Let i be given.
Assume Hi: i ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE i Hi.
We will prove Pi_SNo f 0 = n.
rewrite the current goal using Pi_SNo_0 f (from left to right).
Use symmetry.
An exact proof term for the current goal is H2.
Let k' be given.
Assume Hk': k' ∈ ω.
Let f' be given.
Assume Hf': nonincrfinseq prime_nat k' f'.
Assume H3: Pi_SNo f' k' = n.
We prove the intermediate claim Lf'1: ∀i ∈ k', prime_nat (f' i).
Let i be given.
Assume Hi: i ∈ k'.
Apply Hf' i Hi to the current goal.
Assume H4: prime_nat (f' i).
Assume _.
An exact proof term for the current goal is H4.
We prove the intermediate claim Lf'2: ∀i ∈ k', f' i ∈ ω.
Let i be given.
Assume Hi: i ∈ k'.
Apply Lf'1 i Hi to the current goal.
Assume H.
Apply H to the current goal.
Assume H4: f' i ∈ ω.
Assume _ _.
An exact proof term for the current goal is H4.
Apply andI to the current goal.
We will prove k' = 0.
Apply Empty_eq to the current goal.
Let i be given.
Assume Hi: i ∈ k'.
We will prove False.
We prove the intermediate claim Lf'i1: prime_nat (f' i).
An exact proof term for the current goal is Lf'1 i Hi.
We prove the intermediate claim Lf'i2: f' i ∈ ω.
An exact proof term for the current goal is Lf'2 i Hi.
Apply SNoLt_irref n to the current goal.
We will prove n < n.
rewrite the current goal using H2 (from left to right) at position 1.
We will prove 1 < n.
Apply SNoLtLe_tra 1 (f' i) n SNo_1 to the current goal.
We will prove SNo (f' i).
An exact proof term for the current goal is omega_SNo (f' i) Lf'i2.
We will prove SNo n.
Apply nat_p_SNo to the current goal.
An exact proof term for the current goal is Hn.
We will prove 1 < f' i.
Apply Lf'i1 to the current goal.
Assume H.
Apply H to the current goal.
Assume _.
Assume H4: 1 ∈ f' i.
Assume _.
We will prove 1 < f' i.
An exact proof term for the current goal is ordinal_In_SNoLt (f' i) (nat_p_ordinal (f' i) (omega_nat_p (f' i) Lf'i2)) 1 H4.
We will prove f' i ≤ n.
Apply divides_int_pos_Le (f' i) n to the current goal.
We will prove divides_int (f' i) n.
Apply divides_nat_divides_int to the current goal.
We will prove divides_nat (f' i) n.
rewrite the current goal using H3 (from right to left).
We will prove divides_nat (f' i) (Pi_SNo f' k').
An exact proof term for the current goal is Pi_SNo_divides f' k' (omega_nat_p k' Hk') Lf'2 i Hi.
We will prove 0 < n.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is SNoLt_0_1.
Let i be given.
Assume Hi: i ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE i Hi.
Assume H2: n ≠ 1.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is nat_p_SNo n Hn.
We prove the intermediate claim Lno: ordinal n.
An exact proof term for the current goal is nat_p_ordinal n Hn.
We prove the intermediate claim L1: 1 ∈ n.
Apply ordinal_In_Or_Subq 1 n (nat_p_ordinal 1 nat_1) Lno to the current goal.
Assume H3: 1 ∈ n.
An exact proof term for the current goal is H3.
Assume H3: n ⊆ 1.
We will prove False.
Apply H2 to the current goal.
Apply set_ext to the current goal.
An exact proof term for the current goal is H3.
We will prove 1 ⊆ n.
Let i be given.
Assume Hi: i ∈ 1.
Apply cases_1 i Hi to the current goal.
We will prove 0 ∈ n.
An exact proof term for the current goal is H1.
We prove the intermediate claim L2: ∃p, ordinal p ∧ (prime_nat p ∧ divides_nat p n) ∧ ∀q ∈ p, ¬ (prime_nat q ∧ divides_nat q n).
Apply least_ordinal_ex to the current goal.
We will prove ∃p, ordinal p ∧ (prime_nat p ∧ divides_nat p n).
Apply prime_nat_divisor_ex n Hn L1 to the current goal.
Let p be given.
Assume H.
Apply H to the current goal.
Assume H3: prime_nat p.
Assume H4: divides_nat p n.
We use p to witness the existential quantifier.
Apply andI to the current goal.
We will prove ordinal p.
Apply H3 to the current goal.
Assume H _.
Apply H to the current goal.
Assume H5: p ∈ ω.
Assume _.
An exact proof term for the current goal is nat_p_ordinal p (omega_nat_p p H5).
Apply andI to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is H4.
Apply L2 to the current goal.
Let p be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume Hpo: ordinal p.
Assume H.
Apply H to the current goal.
Assume Hpp: prime_nat p.
Assume Hpn: divides_nat p n.
Assume Hpleast: ∀q ∈ p, ¬ (prime_nat q ∧ divides_nat q n).
Apply Hpp to the current goal.
Assume H _.
Apply H to the current goal.
Assume HpN: p ∈ ω.
Assume H1p: 1 ∈ p.
Apply Hpn to the current goal.
Assume _ H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ ω.
rewrite the current goal using mul_nat_mul_SNo p HpN m Hm (from left to right).
Assume Hpm: p * m = n.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is omega_SNo m Hm.
We prove the intermediate claim LmN: nat_p m.
An exact proof term for the current goal is omega_nat_p m Hm.
We prove the intermediate claim Lmo: ordinal m.
An exact proof term for the current goal is nat_p_ordinal m LmN.
We prove the intermediate claim LpS: SNo p.
An exact proof term for the current goal is omega_SNo p HpN.
We prove the intermediate claim LpN: nat_p p.
An exact proof term for the current goal is omega_nat_p p HpN.
We prove the intermediate claim Lpo: ordinal p.
An exact proof term for the current goal is nat_p_ordinal p LpN.
We prove the intermediate claim Lmp: m * p = n.
rewrite the current goal using mul_SNo_com m p LmS LpS (from left to right).
An exact proof term for the current goal is Hpm.
We prove the intermediate claim L1p: 1 < p.
Apply ordinal_In_SNoLt p Hpo 1 to the current goal.
We will prove 1 ∈ p.
An exact proof term for the current goal is H1p.
We prove the intermediate claim Lmpos: 0 < m.
Apply SNoLeE 0 m SNo_0 LmS (omega_nonneg m Hm) to the current goal.
Assume H3: 0 < m.
An exact proof term for the current goal is H3.
Assume H3: 0 = m.
We will prove False.
We prove the intermediate claim Ln0: n = 0.
rewrite the current goal using Hpm (from right to left).
We will prove p * m = 0.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is mul_SNo_zeroR p LpS.
Apply In_irref n to the current goal.
We will prove n ∈ n.
rewrite the current goal using Ln0 (from left to right) at position 1.
An exact proof term for the current goal is H1.
We prove the intermediate claim L3: m < n.
rewrite the current goal using Lmp (from right to left).
We will prove m < m * p.
rewrite the current goal using mul_SNo_oneR m LmS (from right to left) at position 1.
We will prove m * 1 < m * p.
Apply pos_mul_SNo_Lt m 1 p LmS Lmpos SNo_1 LpS L1p to the current goal.
We prove the intermediate claim L4: m ∈ n.
An exact proof term for the current goal is ordinal_SNoLt_In m n Lmo Lno L3.
We prove the intermediate claim L5: 0 ∈ m.
An exact proof term for the current goal is ordinal_SNoLt_In 0 m ordinal_Empty Lmo Lmpos.
Apply IH m L4 L5 to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
Assume H.
Apply H to the current goal.
Let f be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume Hf: nonincrfinseq prime_nat k f.
Assume Hfkm: Pi_SNo f k = m.
Assume Huniq: ∀k' ∈ ω, ∀f' : set → set, nonincrfinseq prime_nat k' f' → Pi_SNo f' k' = m → k' = k ∧ ∀i ∈ k, f' i = f i.
We prove the intermediate claim LkN: nat_p k.
An exact proof term for the current goal is omega_nat_p k Hk.
We prove the intermediate claim Lf1: ∀i ∈ k, prime_nat (f i).
Let i be given.
Assume Hi: i ∈ k.
Apply Hf i Hi to the current goal.
Assume H3: prime_nat (f i).
Assume _.
An exact proof term for the current goal is H3.
We prove the intermediate claim Lf2: ∀i ∈ k, f i ∈ ω.
Let i be given.
Assume Hi: i ∈ k.
Apply Lf1 i Hi to the current goal.
Assume H.
Apply H to the current goal.
Assume H3: f i ∈ ω.
Assume _ _.
An exact proof term for the current goal is H3.
We prove the intermediate claim Lg: ∃g : set → set, g k = p ∧ ∀i ∈ k, g i = f i.
Set g to be the term λi ⇒ if i ∈ k then f i else p of type set → set.
We use g to witness the existential quantifier.
Apply andI to the current goal.
We will prove g k = p.
An exact proof term for the current goal is If_i_0 (k ∈ k) (f k) p (In_irref k).
Let i be given.
Assume Hi: i ∈ k.
We will prove g i = f i.
An exact proof term for the current goal is If_i_1 (i ∈ k) (f i) p Hi.
Apply Lg to the current goal.
Let g be given.
Assume H.
Apply H to the current goal.
Assume Hgk: g k = p.
Assume Hgi: ∀i ∈ k, g i = f i.
We will prove ∃k ∈ ω, ∃f : set → set, nonincrfinseq prime_nat k f ∧ Pi_SNo f k = n ∧ ∀k' ∈ ω, ∀f' : set → set, nonincrfinseq prime_nat k' f' → Pi_SNo f' k' = n → k' = k ∧ ∀i ∈ k, f' i = f i.
We use (ordsucc k) to witness the existential quantifier.
Apply andI to the current goal.
We will prove ordsucc k ∈ ω.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Hk.
We use g to witness the existential quantifier.
Apply and3I to the current goal.
We will prove nonincrfinseq prime_nat (ordsucc k) g.
Let i be given.
Assume Hi: i ∈ ordsucc k.
Apply ordsuccE k i Hi to the current goal.
Assume H3: i ∈ k.
We will prove prime_nat (g i) ∧ ∀j ∈ i, g i ≤ g j.
rewrite the current goal using Hgi i H3 (from left to right).
We will prove prime_nat (f i) ∧ ∀j ∈ i, f i ≤ g j.
Apply Hf i H3 to the current goal.
Assume H4: prime_nat (f i).
Assume H5: ∀j ∈ i, f i ≤ f j.
Apply andI to the current goal.
An exact proof term for the current goal is H4.
Let j be given.
Assume Hj: j ∈ i.
We will prove f i ≤ g j.
We prove the intermediate claim Lj: j ∈ k.
An exact proof term for the current goal is nat_trans k LkN i H3 j Hj.
rewrite the current goal using Hgi j Lj (from left to right).
An exact proof term for the current goal is H5 j Hj.
Assume H3: i = k.
We will prove prime_nat (g i) ∧ ∀j ∈ i, g i ≤ g j.
rewrite the current goal using H3 (from left to right).
rewrite the current goal using Hgk (from left to right).
We will prove prime_nat p ∧ ∀j ∈ k, p ≤ g j.
Apply andI to the current goal.
An exact proof term for the current goal is Hpp.
Let j be given.
Assume Hj: j ∈ k.
rewrite the current goal using Hgi j Hj (from left to right).
We will prove p ≤ f j.
We prove the intermediate claim LfjN: nat_p (f j).
An exact proof term for the current goal is omega_nat_p (f j) (Lf2 j Hj).
We prove the intermediate claim LfjS: SNo (f j).
An exact proof term for the current goal is nat_p_SNo (f j) LfjN.
We prove the intermediate claim Lfjo: ordinal (f j).
An exact proof term for the current goal is nat_p_ordinal (f j) LfjN.
Apply SNoLtLe_or (f j) p LfjS LpS to the current goal.
Assume H4: f j < p.
We will prove False.
Apply Hpleast (f j) to the current goal.
We will prove f j ∈ p.
Apply ordinal_SNoLt_In (f j) p Lfjo Lpo to the current goal.
We will prove f j < p.
An exact proof term for the current goal is H4.
Apply andI to the current goal.
We will prove prime_nat (f j).
An exact proof term for the current goal is Lf1 j Hj.
We will prove divides_nat (f j) n.
Apply divides_nat_tra (f j) m n to the current goal.
We will prove divides_nat (f j) m.
rewrite the current goal using Hfkm (from right to left).
We will prove divides_nat (f j) (Pi_SNo f k).
An exact proof term for the current goal is Pi_SNo_divides f k LkN Lf2 j Hj.
We will prove divides_nat m n.
rewrite the current goal using Lmp (from right to left).
We will prove divides_nat m (m * p).
An exact proof term for the current goal is divides_nat_mul_SNo_R m Hm p HpN.
Assume H4: p ≤ f j.
An exact proof term for the current goal is H4.
We will prove Pi_SNo g (ordsucc k) = n.
rewrite the current goal using Pi_SNo_S g k LkN (from left to right).
We will prove Pi_SNo g k * g k = n.
rewrite the current goal using Lmp (from right to left).
We will prove Pi_SNo g k * g k = m * p.
Use f_equal.
We will prove Pi_SNo g k = m.
rewrite the current goal using Pi_SNo_eq g f k LkN Hgi (from left to right).
We will prove Pi_SNo f k = m.
An exact proof term for the current goal is Hfkm.
We will prove g k = p.
An exact proof term for the current goal is Hgk.
We will prove ∀k' ∈ ω, ∀g' : set → set, nonincrfinseq prime_nat k' g' → Pi_SNo g' k' = n → k' = ordsucc k ∧ ∀i ∈ ordsucc k, g' i = g i.
Let k' be given.
Assume Hk': k' ∈ ω.
Let g' be given.
Assume Hg': nonincrfinseq prime_nat k' g'.
Assume Hg'k': Pi_SNo g' k' = n.
We prove the intermediate claim Lg'1: ∀i ∈ k', prime_nat (g' i).
Let i be given.
Assume Hi: i ∈ k'.
Apply Hg' i Hi to the current goal.
Assume H4: prime_nat (g' i).
Assume _.
An exact proof term for the current goal is H4.
We prove the intermediate claim Lg'2: ∀i ∈ k', g' i ∈ ω.
Let i be given.
Assume Hi: i ∈ k'.
Apply Lg'1 i Hi to the current goal.
Assume H.
Apply H to the current goal.
Assume H4: g' i ∈ ω.
Assume _ _.
An exact proof term for the current goal is H4.
We will prove k' = ordsucc k ∧ ∀i ∈ ordsucc k, g' i = g i.
We prove the intermediate claim Lk'N: nat_p k'.
An exact proof term for the current goal is omega_nat_p k' Hk'.
Apply nat_inv k' Lk'N to the current goal.
Assume Hk': k' = 0.
We will prove False.
Apply H2 to the current goal.
We will prove n = 1.
rewrite the current goal using Hg'k' (from right to left).
rewrite the current goal using Hk' (from left to right).
Apply Pi_SNo_0 to the current goal.
Assume H.
Apply H to the current goal.
Let k'' be given.
Assume H.
Apply H to the current goal.
Assume Hk'': nat_p k''.
Assume Hk'k'': k' = ordsucc k''.
We prove the intermediate claim L6: nonincrfinseq prime_nat k'' g'.
Let i be given.
Assume Hi: i ∈ k''.
We will prove prime_nat (g' i) ∧ ∀j ∈ i, g' i ≤ g' j.
We prove the intermediate claim Li: i ∈ k'.
rewrite the current goal using Hk'k'' (from left to right).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
An exact proof term for the current goal is Hg' i Li.
We prove the intermediate claim LPg'k''N: Pi_SNo g' k'' ∈ ω.
Apply Pi_SNo_In_omega g' k'' Hk'' to the current goal.
Let i be given.
Assume Hi: i ∈ k''.
We prove the intermediate claim Li: i ∈ k'.
rewrite the current goal using Hk'k'' (from left to right).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
An exact proof term for the current goal is Lg'2 i Li.
We prove the intermediate claim LPg'k''S: SNo (Pi_SNo g' k'').
An exact proof term for the current goal is omega_SNo (Pi_SNo g' k'') LPg'k''N.
We prove the intermediate claim L7: g' k'' = p.
We prove the intermediate claim L7a: prime_nat (g' k'') ∧ ∀j ∈ k'', g' k'' ≤ g' j.
Apply Hg' k'' to the current goal.
We will prove k'' ∈ k'.
rewrite the current goal using Hk'k'' (from left to right).
Apply ordsuccI2 to the current goal.
Apply L7a to the current goal.
Assume Hg'k''P: prime_nat (g' k'').
Assume Hg'k''minimal: ∀j ∈ k'', g' k'' ≤ g' j.
Apply Hg'k''P to the current goal.
Assume H _.
Apply H to the current goal.
Assume H4: g' k'' ∈ ω.
Assume H5: 1 ∈ g' k''.
We prove the intermediate claim Lg'k''N: nat_p (g' k'').
An exact proof term for the current goal is omega_nat_p (g' k'') H4.
We prove the intermediate claim Lg'k''o: ordinal (g' k'').
An exact proof term for the current goal is nat_p_ordinal (g' k'') Lg'k''N.
We prove the intermediate claim Lg'k''S: SNo (g' k'').
An exact proof term for the current goal is nat_p_SNo (g' k'') Lg'k''N.
We prove the intermediate claim L7b: divides_nat (g' k'') n.
rewrite the current goal using Hg'k' (from right to left).
We will prove divides_nat (g' k'') (Pi_SNo g' k').
rewrite the current goal using Hk'k'' (from left to right).
rewrite the current goal using Pi_SNo_S g' k'' Hk'' (from left to right).
We will prove divides_nat (g' k'') (Pi_SNo g' k'' * g' k'').
Apply divides_nat_mul_SNo_L to the current goal.
An exact proof term for the current goal is LPg'k''N.
An exact proof term for the current goal is H4.
We prove the intermediate claim L7c: divides_int p (Pi_SNo g' k').
Apply Hg'k' (λu v ⇒ divides_int p v) to the current goal.
We will prove divides_int p n.
Apply divides_nat_divides_int to the current goal.
An exact proof term for the current goal is Hpn.
We prove the intermediate claim L7d: divides_int p (Pi_SNo g' k'') ∨ divides_int p (g' k'').
Apply Euclid_lemma p Hpp to the current goal.
We will prove Pi_SNo g' k'' ∈ int.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is LPg'k''N.
We will prove g' k'' ∈ int.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is H4.
We will prove divides_int p (Pi_SNo g' k'' * g' k'').
rewrite the current goal using Pi_SNo_S g' k'' Hk'' (from right to left).
We will prove divides_int p (Pi_SNo g' (ordsucc k'')).
rewrite the current goal using Hk'k'' (from right to left).
An exact proof term for the current goal is L7c.
We prove the intermediate claim L7e: ∀i ∈ k'', g' i ∈ int.
Let i be given.
Assume Hi.
Apply Subq_omega_int to the current goal.
Apply Lg'2 to the current goal.
We will prove i ∈ k'.
rewrite the current goal using Hk'k'' (from left to right).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
Apply L7d to the current goal.
Assume H6: divides_int p (Pi_SNo g' k'').
We will prove g' k'' = p.
Apply SNoLt_trichotomy_or_impred (g' k'') p Lg'k''S LpS to the current goal.
Assume H7: g' k'' < p.
We will prove False.
Apply Hpleast (g' k'') to the current goal.
We will prove g' k'' ∈ p.
An exact proof term for the current goal is ordinal_SNoLt_In (g' k'') p Lg'k''o Lpo H7.
We will prove prime_nat (g' k'') ∧ divides_nat (g' k'') n.
Apply andI to the current goal.
An exact proof term for the current goal is Hg'k''P.
An exact proof term for the current goal is L7b.
Assume H7: g' k'' = p.
An exact proof term for the current goal is H7.
Assume H7: p < g' k''.
We will prove False.
Apply Euclid_lemma_Pi_SNo g' p Hpp k'' Hk'' L7e H6 to the current goal.
Let j be given.
Assume H.
Apply H to the current goal.
Assume Hj: j ∈ k''.
Assume H8: divides_int p (g' j).
We prove the intermediate claim L7f: prime_nat (g' j).
Apply Lg'1 to the current goal.
rewrite the current goal using Hk'k'' (from left to right).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hj.
We prove the intermediate claim L7g: p = g' j.
An exact proof term for the current goal is divides_int_prime_nat_eq p (g' j) Hpp L7f H8.
Apply SNoLt_irref p to the current goal.
We will prove p < p.
Apply SNoLtLe_tra p (g' k'') p LpS Lg'k''S LpS H7 to the current goal.
We will prove g' k'' ≤ p.
rewrite the current goal using L7g (from left to right).
We will prove g' k'' ≤ g' j.
Apply Hg'k''minimal to the current goal.
We will prove j ∈ k''.
An exact proof term for the current goal is Hj.
Assume H6: divides_int p (g' k'').
We will prove g' k'' = p.
Use symmetry.
Apply divides_int_prime_nat_eq p (g' k'') Hpp to the current goal.
We will prove prime_nat (g' k'').
Apply Lg'1 to the current goal.
rewrite the current goal using Hk'k'' (from left to right).
Apply ordsuccI2 to the current goal.
We will prove divides_int p (g' k'').
An exact proof term for the current goal is H6.
We prove the intermediate claim L8: Pi_SNo g' k'' = m.
Apply mul_SNo_nonzero_cancel p (Pi_SNo g' k'') m to the current goal.
We will prove SNo p.
An exact proof term for the current goal is LpS.
We will prove p ≠ 0.
Assume H4: p = 0.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
rewrite the current goal using H4 (from right to left) at position 2.
We will prove 0 < p.
An exact proof term for the current goal is SNoLt_tra 0 1 p SNo_0 SNo_1 LpS SNoLt_0_1 L1p.
We will prove SNo (Pi_SNo g' k'').
An exact proof term for the current goal is LPg'k''S.
We will prove SNo m.
An exact proof term for the current goal is LmS.
We will prove p * Pi_SNo g' k'' = p * m.
rewrite the current goal using Hpm (from left to right).
We will prove p * Pi_SNo g' k'' = n.
rewrite the current goal using Hg'k' (from right to left).
We will prove p * Pi_SNo g' k'' = Pi_SNo g' k'.
rewrite the current goal using Hk'k'' (from left to right).
We will prove p * Pi_SNo g' k'' = Pi_SNo g' (ordsucc k'').
rewrite the current goal using Pi_SNo_S g' k'' Hk'' (from left to right).
We will prove p * Pi_SNo g' k'' = Pi_SNo g' k'' * g' k''.
rewrite the current goal using L7 (from left to right).
We will prove p * Pi_SNo g' k'' = Pi_SNo g' k'' * p.
An exact proof term for the current goal is mul_SNo_com p (Pi_SNo g' k'') LpS LPg'k''S.
Apply Huniq k'' (nat_p_omega k'' Hk'') g' L6 L8 to the current goal.
Assume H3: k'' = k.
Assume H4: ∀i ∈ k, g' i = f i.
We will prove k' = ordsucc k ∧ ∀i ∈ ordsucc k, g' i = g i.
Apply andI to the current goal.
We will prove k' = ordsucc k.
rewrite the current goal using Hk'k'' (from left to right).
Use f_equal.
An exact proof term for the current goal is H3.
Let i be given.
Assume Hi: i ∈ ordsucc k.
Apply ordsuccE k i Hi to the current goal.
Assume H5: i ∈ k.
We will prove g' i = g i.
rewrite the current goal using Hgi i H5 (from left to right).
We will prove g' i = f i.
An exact proof term for the current goal is H4 i H5.
Assume H5: i = k.
We will prove g' i = g i.
rewrite the current goal using H5 (from left to right).
rewrite the current goal using Hgk (from left to right).
We will prove g' k = p.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is L7.
∎