proposition: Lemma sumList_rel_left_total : forall (A : Type)(rel : A -> Rat -> Prop)(ls : list A), (forall a, In a ls -> exists r, rel a r) -> exists r, sumList_rel rel ls r.
proof: Proof. induction ls; intuition; simpl in *. exists 0. econstructor. intuition. edestruct H. left. eauto. edestruct IHls. intuition. econstructor. econstructor. eauto. eauto. eapply eqRat_refl. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation