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