proposition: Lemma CRscal_mult_scal_one : forall a n, (n ** one) * a == n ** a.
proof: Proof. intros a 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