proposition: Lemma ratInverse_scale_sum_1 : forall (A : Set)(ls : list A)(f : A -> Rat), (forall a, In a ls -> ~f a == 0) -> length ls > O -> sumList ls (fun a => (ratInverse (sumList ls f)) * (f a)) == 1.
proof: Proof. intuition. rewrite sumList_factor_constant_l. eapply ratInverse_prod_1. intuition. destruct ls; simpl in *. lia. eapply sumList_0 in H1. eapply H. eauto. eauto. simpl. eauto. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec