proposition: Lemma fold_plus_sym : forall (seq: list nat) (default: nat), List.fold_right plus default seq = List.fold_left plus seq default.
proof: Proof. intros; rewrite <- fold_left_rev_right. revert default; induction seq; simpl; eauto; intros. rewrite fold_right_app; simpl; rewrite <- IHseq. clear IHseq; revert a default; induction seq; simpl; intros; auto with arith. rewrite <- IHseq. rewrite Nat.add_comm, <- Nat.add_assoc; f_equal. rewrite Nat.add_comm; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts