proposition: Lemma FFK_correct (p q : positive) (fp fq : Fchain): Fchain_correct p fp -> Fchain_correct q fq -> Fchain_proper fp -> Fchain_proper fq -> Kchain_correct (p * q ) p (FFK fp fq).
proof: Proof. intros;red; rewrite Pos2Nat.inj_mul; now apply FFK_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)