proposition: Lemma exponent_nat_neq_0 : forall c: chain, parametric c -> the_exponent_nat c <> 0.
proof: Proof. intros c Hc; red in Hc; unfold the_exponent_nat. generalize (param_correctness_aux nat _ _ eq Natplus c 1). destruct 1. - apply Hc. split;auto. now compute. - unfold chain_apply; rewrite H0. induction (the_exponent_nat c). + now destruct H. + discriminate. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)