proposition: Lemma CRadd_scal_eq_compat : forall a n p, (n ** a) + (p ** a) == (n + p) ** a.
proof: Proof. intros a n p. induction n. simpl; ring. simpl. rewrite <- IHn. ring. Qed.
imports: Type_class_definition Type_class_instance Coq.Relations.Relation_Definitions Lia Arith Nbinomial Setoid