求助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]_ 结束 。 *)