proposition: Lemma k7_3_correct : Kchain_correct 7 3 k7_3.
proof: Proof. intros until M; intros; red; unfold k7_3; 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)