proposition: Lemma param_correctness : forall (p:positive) (c:chain), p = the_exponent c -> parametric c -> chain_correct p c.
proof: Proof. intros; subst p; rewrite exponent_pos_of_nat; auto. red; rewrite exponent_pos2nat;auto. rewrite Pos2Nat.id, <- exponent_pos2nat;auto. apply param_correctness_nat; auto. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)