proposition: Lemma Fcompose_correct_nat : forall fc1 fc2 n1 n2, Fchain_correct_nat n1 fc1 -> Fchain_correct_nat n2 fc2 -> Fchain_proper fc2 -> Fchain_correct_nat (n1 * n2)%nat (Fcompose fc1 fc2).
proof: Proof. unfold Fcompose, Fchain_correct_nat; intros. assert (Fkont_proper M (fun y : A => fc2 A k y)). - intros x y Hxy; apply H1 with E_one M;auto. - rewrite (H _ _ _ _ M (fun y : A => fc2 A k y) H2 a). + rewrite (H0 _ _ _ _ M k Hk). * apply Hk. rewrite power_of_power;auto; rewrite Nat.mul_comm;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)