proposition: Lemma param_correctness_aux : forall (c:chain)(a:A), computation_R A nat (power_R a ) (c A a) (c nat 1%nat) -> power_R a (computation_eval (c A a)) (the_exponent_nat c) .
proof: Proof. intros c a Hc; now apply power_R_is_a_refinement. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)