proposition: Lemma CRsum_add_compat : forall a b n, CRsum (fun i => a i + b i) n == CRsum a n + CRsum b n.
proof: Proof. intros a b n. induction n. simpl; reflexivity. simpl. rewrite IHn. ring. Qed.
imports: Type_class_definition Type_class_instance Coq.Relations.Relation_Definitions Lia Arith Nbinomial Setoid