proposition: Theorem sumList_1_mult : forall (A : Set)(ls : list A), sumList ls (fun _ => 1) == length ls / 1.
proof: Proof. induction ls; intuition. unfold sumList; simpl. reflexivity. rewrite sumList_cons. simpl. rewrite IHls. rewrite ratS_num. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation