proposition: Lemma CRsum_eq_compat_weak : forall a b n, (forall n, a n == b n) -> CRsum a n == CRsum b n.
proof: Proof. intros a b n H. induction n. simpl; apply H. simpl. rewrite IHn. rewrite H. reflexivity. Qed.
imports: Type_class_definition Type_class_instance Coq.Relations.Relation_Definitions Lia Arith Nbinomial Setoid