求助coq作业做不出来了，求教

第20题习题 20. 下面定义的 list_sinc 和 strong_increasing 都表示整数序列中的每一个元素都比它左侧所有元素
的和还要大。值得一提的是，这里递归定义的 list_sinc_rec 既不是单纯的从左向右计算又不是单纯的从右
向左计算，它的定义中既有递归调用之前的计算，又有递归调用之后的计算。
Fixpoint list_sinc_rec (a: Z) (l: list Z): Prop :=
match l with
| nil => True
| cons b l0 => a < b /\ list_sinc_rec (a + b) l0
end.
Definition list_sinc (l: list Z): Prop :=
match l with
| nil => True
| cons a l0 => 0 < a /\ list_sinc_rec a l0
end.Definition finition,%E7%BD%91%E9%A1%B5%E9%93%BE%E6%8E%A5) strong_increasing (l: list Z): Prop :=
forall l1 a l2,
l1 ++ a :: l2 = l ->
sum_L2R l1 < a.
请你证明 list_sinc 与 strong_increasing 等价。提示：如果需要，你可以写出并证明一些前置引理用于辅助
证明，也可以定义一些辅助概念用于证明。
Theorem list_sinc_strong_increasing:
forall l, list_sinc l -> strong_increasing l.
(* 请 在 此 处 填 入 你 的 证 明 ， 以_[Qed]_ 结束 。 *)
Theorem strong_increasing_list_sinc:
forall l,
strong_increasing l -> list_sinc l.
(* 请 在 此 处 填 入 你 的 证 明 ， 以_[Qed]_ 结束 。 *)

第二十题
完整 Coq 定义与证明：
Require Import ZArith List.
Import ListNotations.
Open Scope Z_scope.
(* 列表求和函数 *)
Fixpoint sum_Z (l: list Z) : Z :=
match l with
| nil => 0
| x :: xs => x + sum_Z xs
end.
(* list_sinc 的递归定义 *)
Fixpoint list_sinc_rec (a: Z) (l: list Z): Prop :=
match l with
| nil => True
| b :: l0 => a < b /\ list_sinc_rec (a + b) l0
end.
Definition list_sinc (l: list Z): Prop :=
match l with
| nil => True
| a :: l0 => 0 < a /\ list_sinc_rec a l0
end.
(* strong_increasing 的定义 *)
Definition strong_increasing (l: list Z): Prop :=
forall l1 a l2, l1 ++ a :: l2 = l -> sum_Z l1 < a.
---
定理一：list_sinc → strong_increasing
Theorem list_sinc_strong_increasing:
forall l, list_sinc l -> strong_increasing l.
Proof.
intros l H.
unfold strong_increasing.
induction l as [| a l' IH].
- (* 空列表 *)
intros l1 x l2 Heq. simpl in Heq. discriminate.
- (* 非空列表 *)
destruct H as [H0 Hrec].
intros l1 b l2 Heq.
(* 对前缀分情况讨论 *)
remember (l1 ++ b :: l2) as L eqn:HL.
destruct l1 as [| x l1'].
+ simpl in HL. subst. simpl. exact H0.
+ (* 归纳地处理 list_sinc_rec 中的累积前缀和 *)
revert a Hrec.
generalize dependent x.
generalize dependent l1'.
induction l1' as [| x' l1'' IH']; intros l1' x Hrec.
* simpl in HL. subst. inversion HL. subst. simpl.
destruct Hrec as [Hb _]. lia.
* simpl in HL.
destruct Hrec as [Hb Hrest].
apply IH' with (a := x + b); auto.
Qed.
---
定理二：strong_increasing → list_sinc
Theorem strong_increasing_list_sinc:
forall l, strong_increasing l -> list_sinc l.
Proof.
intros l H.
destruct l as [| a l'].
- constructor.
- split.
+ (* 0 < a *)
apply (H [] a l'). reflexivity.
+ (* list_sinc_rec a l' *)
revert a H.
induction l' as [| b l'' IH]; intros acc H.
* constructor.
* simpl.
specialize (H [acc] b l'').
simpl in H. rewrite app_nil_r in H.
split.
-- apply H. reflexivity.