proposition: Lemma OK87 : Fchain_correct 87 F87.
proof: Proof. unfold F87; change 87 with (10 * (2 ^ 3) + 7)%positive. apply KFF_correct;auto with chains. change 10 with (7 * 1 + 3); apply KFK_correct;auto with chains. change 7 with (3 * 2 ^ 1 + 1)%positive; apply KFK_correct;auto with chains. 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)