proposition: Lemma power_R_is_a_refinement (a:A) : forall(gamma : @computation A) (gamma_nat : @computation nat), computation_R _ _ (power_R a) gamma gamma_nat -> power_R a (computation_eval gamma) (computation_eval (M:= Natplus) gamma_nat).
proof: Proof. induction 1;simpl;[auto | ]. apply H; destruct x_R, y_R; split. unfold mult_op, nat_plus_op. + lia. + apply power_R_Mult; split;auto. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)