proposition: Lemma param_correctness_for_free : any_chain_parametric -> forall p (c : chain) , p = the_exponent c -> chain_correct p c.
proof: Proof. intros H p c H0. rewrite H0. apply param_correctness; trivial. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)