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