proposition: Theorem F3_correct : Fchain_correct 3 F3.
proof: Proof. intros A op E_one E_equiv M k a ; cbn. monoid_simpl M. Abort. End Bad. Definition computation_equiv {A:Type} (op: Mult_op A) (equiv : Equiv A) (c c': @computation A) := computation_execute op c == computation_execute op c'. #[ global ] Instance Comp_equiv {A:Type} (op: Mult_op A) (equiv : Equiv A): Equiv (@computation A) := @computation_equiv A op equiv. #[ global ] Instance comp_equiv_equivalence {A:Type} (op: Mult_op A) (equiv : Equiv A) : Equivalence equiv -> Equivalence (computation_equiv op equiv). Proof. intro H; split; red in equiv. - intro c; red;reflexivity. - intros x y H0; red; symmetry; auto. - intros x y z H0 H1; red; transitivity (computation_execute op y);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)