proposition: Lemma FFK_correct_nat : forall (p q : nat) (fp fq : Fchain), Fchain_correct_nat p fp -> Fchain_correct_nat q fq -> Fchain_proper fp -> Fchain_proper fq -> Kchain_correct_nat (p * q) p (FFK fp fq).
proof: Proof. intros. red;intros. unfold FFK; simpl. add_op_proper M Hop. specialize (H _ _ _ _ M). specialize (H0 _ _ _ _ M). specialize (H1 _ _ _ _ M). specialize (H2 _ _ _ _ M). specialize (H (fun xb : A => fq A (fun y : A => k y xb) xb)). assert (Fkont_proper M (fun xb : A => fq A (fun y : A => k y xb) xb)). - intros x y Hxy ;simpl; red;simpl. apply H2. + intros u v Huv; apply H3; (assumption || reflexivity). + intros u v Huv; apply H3; (assumption || reflexivity). + intros u v Huv; apply H3; (assumption || reflexivity). + assumption. - specialize (H H4 a); rewrite H. specialize (H0 (fun y => k y (a ^ p))). assert (Fkont_proper M (fun y : A => k y (a ^ p))). + red; intros x y Hxy; red; simpl; apply H3; (assumption || reflexivity). + rewrite (H0 H5); apply H3; [| reflexivity]. rewrite (power_of_power M a p q), (Nat.mul_comm q p); reflexivity. 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)