Hello again,

Thanks to the help of this community I have been able to successfully get the `Programs`

module to successfully pull in the necessary predicates in order to prove the well-foundedness of my fixpoint function. The version of the file I am currently dealing with is this:

```
Require Import Nat String List.
Require Import Row.
Require Coq.Program.Tactics.
Require Coq.Program.Wf.
Open Scope list_scope.
Open Scope string_scope.
(*Duplicated for clarity - this inductive definition is in another module in the original*)
Inductive row : Type :=
| Section : list row -> section
.
Inductive section : Type :=
| Section : list row -> section
.
Program Fixpoint get_section (rows:list row) : (list row * list row) :=
match rows with
| nil => (nil, nil)
| EmptyRow :: rs => (nil, rs)
| DataRow r :: rs =>
let (sect, rst) := get_section rs in
((DataRow r :: sect), rst)
end.
Theorem succ_x_less_than_succ_succ_succ_x : forall (x : nat),
S x < S (S (S x)).
Proof.
intros. auto.
Defined.
Theorem succ_x_lt_succ_succ_x : forall (x:nat), S x < S (S x).
Proof. auto. Defined.
Program Fixpoint get_sections (rows : list row) {measure (length rows) }
: list section :=
match rows with
| nil => nil
| EmptyRow :: rs => get_sections rs
| DataRow r :: rs =>
match get_section rs with
(*Section with just a header at the end of the sheet*)
| (nil, nil) => Section (DataRow r :: nil) :: nil
(*Section with just a header in the middle or beginning of sheet*)
| (nil, rest) => (Section (DataRow r :: nil)) :: get_sections rest
(*Section with datas*)
| (rest_of_sect, rest) =>
let sect := DataRow r :: rest_of_sect in
(Section sect) :: get_sections rest
end
end.
Next Obligation.
destruct rest.
{ apply PeanoNat.Nat.lt_0_succ. }
{ induction rs.
{ discriminate. }
{ simpl. destruct a.
{ simpl in Heq_anonymous. inversion Heq_anonymous. simpl.
apply succ_x_less_than_succ_succ_succ_x. }
{ simpl in Heq_anonymous.
```

This function takes a list of rows (of a CSV) and converts them into a list of Sections, separated by blank rows. More visually:

```
[
DataRow ["Doc"; "Citation"];
DataRow ["val11"; "val12"];
DataRow ["val21"; "val22"];
EmptyRow;
DataRow ["Type"; "Field"; "Size"];
DataRow ["val13"; "val14"; "val15"];
DataRow ["val23"; "val24"; "val25"];
]
```

to

```
[
Section [
DataRow ["Doc"; "Citation"];
DataRow ["val11"; "val12"];
DataRow ["val21"; "val22"];
];
Section [
DataRow ["Type"; "Field"; "Size"];
DataRow ["val13"; "val14"; "val15"];
DataRow ["val23"; "val24"; "val25"];
]
]
```

As you can see at the end of the Coq module I have left the proof obligation unfinished as I have run into the following context with which I’m not sure how to proceed:

```
- rs : list row
- get_sections : forall rows : list row,
Datatypes.length rows < Datatypes.length (DataRow r :: DataRow l :: rs) -> list section
- r0 : row
- rest : list row
- H : (nil, nil) <> (nil, r0 :: rest)
- Heq_anonymous : (nil, r0 :: rest) = (let (sect, rst) := get_section rs in (DataRow l :: sect, rst))
- IHrs : (forall rows : list row, Datatypes.length rows < Datatypes.length (DataRow r :: rs) -> list section) ->
(nil, r0 :: rest) = get_section rs -> Datatypes.length (r0 :: rest) < Datatypes.length (DataRow r :: rs)
============================
S (Datatypes.length rest) < S (S (Datatypes.length rs))
```

My understanding of how to solve this would suggest to me that I need to show that:

- given a list of rows,
- and a function that turns it into a list of sections,

with the inductive hypothesis on `rs`

(`IHrs`

) I can successfully construct a proof that solves the goal, modulo the inequalities the previous theorems were defined for. It would seem that I have all of this in my context as propositions that I would want to compose together but in my reading through the Coq documentation I’ve not come across something that looks like that yet. Is that what I need to do to solve this goal or am I fundamentally misunderstanding how to solve this goal? Can one compose propositions in Coq and if so, how?