proposition: Lemma CRmul_scal_compat : forall a b n, n ** a * b == a * (n ** 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