proposition: Lemma FK_correct : forall (p: positive) (Fp : Fchain), Fchain_correct p Fp -> Fchain_proper Fp -> Kchain_correct p 1 (FK Fp).
proof: Proof. intros;red; unfold FK; red; intros until M;intros k H1 a. specialize (H _ _ _ _ M (fun y : A => k y a)). specialize (H0 _ _ _ _ M); add_op_proper M Hop. assert (Fkont_proper M (fun y : A => k y a)). - intros x y Hxy; apply H1; (assumption || reflexivity). - specialize (H H2 a);rewrite H;apply H1. + reflexivity. + generalize (power_eq3 a);simpl;now symmetry. 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)