proposition: Remark power_R_Mult : forall a x y i j, power_R a x i -> power_R a y j -> power_R a (x * y) (i+j)%nat.
proof: Proof. simpl; intros a x y i j H H0; destruct H, H0; split. - lia. - add_op_proper M H; rewrite H1, H2, power_of_plus; reflexivity. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)