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