proposition: Lemma Fcompose_correct : forall f1 f2 n1 n2, Fchain_correct n1 f1 -> Fchain_correct n2 f2 -> Fchain_correct (n1 * n2) (Fcompose f1 f2).
proof: Proof. unfold Fchain_correct, Fcompose, Fchain_correct_nat; intros. specialize (H _ _ _ _ M (fun y : A => f2 A k y) ). specialize (H0 _ _ _ _ M). rewrite H. rewrite H0. apply Hk. rewrite Pos2Nat.inj_mul. rewrite power_of_power. rewrite Nat.mul_comm;reflexivity. auto. intros x y Hxy; red. Abort. End Bad2. Module Bad3. Class Fchain_proper (fc : Fchain) := Fchain_proper_bad_prf : forall `(M : @EMonoid A op E_one E_equiv) k , Fkont_proper M k -> forall x y, x == y -> @computation_equiv _ op E_equiv (fc A k x) (fc A k y). #[ global ] Instance Fcompose_proper (f1 f2 : Fchain) (_ : Fchain_proper f1) (_ : Fchain_proper f2) : Fchain_proper (Fcompose f1 f2). Proof. intros until M;intros k Hk x y Hxy; unfold Fcompose;cbn. apply (H _ _ _ _ M); auto. intros u v Huv;apply (H0 _ _ _ _ M);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)