proposition: Lemma param_correctness_nat (c: chain) : parametric c -> chain_correct_nat (the_exponent_nat c) c.
proof: Proof. intros Hc ; split. - now apply exponent_nat_neq_0. - intros A op one Aeq M a ; unfold chain_apply. apply param_correctness_aux, Hc. split. + discriminate. + simpl; rewrite (Eone_right (EMonoid:=M)); reflexivity. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)