proposition: Lemma K2F_correct : forall kc n p, Kchain_correct n p kc -> Fchain_correct n (K2F kc).
proof: Proof. red;intros; unfold K2F, Fchain_correct. apply K2F_correct_nat with (Pos.to_nat p); apply H. 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)