proposition: Lemma K2F_correct_nat : forall knp n p, Kchain_correct_nat n p knp -> Fchain_correct_nat n (K2F knp).
proof: Proof. red;intros; unfold K2F; apply (H _ _ _ _ M (fun x y => k x)); intros x1 y1 H1 x2 y2 H2; apply Hk; 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)