proposition: Lemma KFK_correct : forall (b q r : positive) (kbr : Kchain) (fq : Fchain), Kchain_correct b r kbr -> Fchain_correct q fq -> Kchain_proper kbr -> Fchain_proper fq -> Kchain_correct (b * q + r) b (KFK kbr fq).
proof: Proof. red; intros; rewrite Pos2Nat.inj_add, Pos2Nat.inj_mul; apply KFK_correct_nat;assumption. 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)