proposition: Lemma Kchain_correct_conv (kc : Kchain) (n p : nat) : 0%nat <> n -> 0%nat <> p -> Kchain_correct_nat n p kc -> Kchain_correct (Pos.of_nat n) (Pos.of_nat p) kc.
proof: Proof. red; intros; repeat rewrite Nat2Pos.id; auto. Qed.
imports: Coq(Inverse_Image Inclusion Wf_nat NArith Arith PArith Recdef Wf_nat Lexicographic_Product Lia) additions(Addition_Chains Compatibility More_on_positive Wf_transparent Dichotomy BinaryStrat) Coq(Lia)