proposition: Lemma sumList_rel_factor_constant : forall (p1 p2 : posnat) (A : Type)(rel : A -> Rat -> Prop)(ls : list A) r, sumList_rel (fun a r' => rel a (r' * (RatIntro p1 p2))) ls (r * (RatIntro p2 p1)) -> sumList_rel rel ls r.
proof: Proof. induction ls; intuition. inversion H; subst; clear H. apply ratMult_0 in H0. destruct H0. econstructor; trivial. exfalso. eapply rat_num_nz; [idtac | eapply H]. eapply posnat_pos. inversion H; clear H; subst. symmetry in H5. apply ratMult_inverse in H5. rewrite ratMult_distrib_r in H5. symmetry in H5. econstructor; eauto. eapply IHls. eapply sumList_rel_body_eq. eapply H2. intuition. rewrite ratMult_assoc. rewrite <- ratMult_1_r at 1. eapply ratMult_eqRat_compat; intuition. rewrite <- ratMult_num_den. symmetry. eapply num_dem_same_rat1. unfold posnatMult, natToPosnat, posnatToNat. destruct p1. destruct p2. apply Nat.mul_comm. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation