proposition: Lemma KFF_correct_nat : Fchain_correct_nat (b * q + r)%nat (KFF kbr fq).
proof: Proof. apply K2F_correct_nat with b; apply KFK_correct_nat. 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)