proposition: Lemma k3_1_correct : Kchain_correct 3 1 k3_1.
proof: Proof. intros until M;intros k H a. unfold k3_1; simpl; apply H; monoid_simpl M;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)