proposition: Lemma Fcompose_correct : forall fc1 fc2 n1 n2, Fchain_correct n1 fc1 -> Fchain_correct n2 fc2 -> Fchain_proper fc2 -> Fchain_correct (n1 * n2) (Fcompose fc1 fc2).
proof: Proof. unfold Fchain_correct; intros. rewrite Pos2Nat.inj_mul. apply Fcompose_correct_nat;auto. 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)