fact: Definition Kchain_correct_nat (n p : nat) (kc : Kchain) := forall (A : Type) (op : Mult_op A) (E_one : A) (E_equiv : Equiv A) (M : EMonoid op E_one E_equiv) (k : Kkont A), Kkont_proper M k -> forall (a : A) , computation_execute op (kc A k a) == computation_execute op (k (a ^ n) (a ^ p)).
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)