proposition: Lemma k3_1_proper : Kchain_proper k3_1.
proof: Proof. intros until M; intros k k' x y H H0 H1 H2. unfold k3_1;simpl. apply H1;auto. add_op_proper M H3; rewrite H2; 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)