proposition: Lemma exponent_pos_of_nat : forall c: chain, parametric c -> the_exponent c = Pos.of_nat (the_exponent_nat c).
proof: Proof. intros c Hc; rewrite exponent_pos2nat;auto. now rewrite Pos2Nat.id. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)