proposition: Lemma KFK_proper : Kchain_proper (KFK kbr fq).
proof: Proof. intros until M; intros k k' x y Hk Hk' ; unfold KFK; simpl. add_op_proper M Hop. specialize (Hbr_prop _ _ _ _ M). specialize (Hq_prop _ _ _ _ M). red; simpl; intros; apply Hbr_prop;auto. - intros x1 y1 Hx1 x2 y2 Hx2; apply Hq_prop;auto. + red; intros;simpl; intros x' y' H'; red;simpl; apply Hk. rewrite H';reflexivity. reflexivity. + intros x' y' H'; red;simpl; apply Hk. rewrite H';reflexivity. reflexivity. + intros y0 y3 H3;red;simpl; apply Hk. rewrite H3,Hx2;reflexivity. assumption. - red;intros;intros u v Huv w t Hwt. apply Hq_prop;auto. + intros X Y HXY;red;simpl; apply Hk'. * rewrite HXY;reflexivity. * reflexivity. + intros X Y HXY;red;simpl; apply Hk'. * rewrite HXY;reflexivity. * reflexivity. + red;intros;red;simpl; apply Hk';auto. rewrite H1, Hwt; reflexivity. - red;intros;apply Hq_prop;auto. + intros X Y HXY;red;simpl; apply Hk. * rewrite HXY;reflexivity. * reflexivity. + intros X Y HXY;red;simpl; apply Hk'. * rewrite HXY;reflexivity. * reflexivity. + red;intros;red;simpl; apply H; auto. * rewrite H2, H3;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)