proposition: Lemma exponent_pos2nat : forall c: chain, parametric c -> the_exponent_nat c = Pos.to_nat (the_exponent c).
proof: Proof. intros c X; generalize (X nat positive (fun n p => n = Pos.to_nat p) 1 xH (refl_equal 1)). unfold the_exponent, the_exponent_nat, chain_execute, chain_apply. generalize (c nat 1), (c _ 1%positive); induction 1. - cbn; assumption. - apply (H (x₁ + y₁)%nat (x₂ + y₂)%positive); rewrite Pos2Nat.inj_add; now subst. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)