proposition: Lemma CRsum_reindex : forall n f, f O + CRsum (fun k => f (S k)) n == CRsum f (S n).
proof: Proof. intros n f. induction n. simpl; ring. do 2 rewrite CRsum_simpl. rewrite <- IHn. ring. Qed.
imports: Type_class_definition Type_class_instance Coq.Relations.Relation_Definitions Lia Arith Nbinomial Setoid