proposition: Lemma CRsum_scal_compat : forall x f n, x * CRsum f n == CRsum (fun n => x * f n) n.
proof: Proof. intros a b n. induction n. simpl; reflexivity. simpl. ring_simplify. rewrite IHn. reflexivity. Qed.
imports: Type_class_definition Type_class_instance Coq.Relations.Relation_Definitions Lia Arith Nbinomial Setoid