proposition: Lemma KFK_correct_nat : Kchain_correct_nat (b * q + r)%nat b (KFK kbr fq).
proof: Proof. intros until M; intros k H a; unfold KFK; simpl. add_op_proper M Hop. specialize (Hq _ _ _ _ M). specialize (Hbr_prop _ _ _ _ M). specialize (Hq_prop _ _ _ _ M). specialize (Hbr _ _ _ _ M (fun xb xr : A => fq A (fun y : A => z <--- y times xr; k z xb) xb)). assert (Kkont_proper M (fun xb xr : A => fq A (fun y : A => z <--- y times xr; k z xb) xb)). - intros x y Hxy z t Hzt;simpl; red;simpl. assert (forall X Y, X == Y -> computation_equiv op E_equiv ((fun y0 : A => z0 <--- y0 times z; k z0 x) X) ((fun y0 : A => z0 <--- y0 times t; k z0 y) Y)). + intros; simpl; red; simpl; apply H; auto. rewrite H0, Hzt; reflexivity. + specialize (H0 x y Hxy); red in H0; simpl; simpl in H0. assert (Proper (computation_equiv op E_equiv ==> equiv) (computation_execute op)). * intros X Y HXY; red in HXY; auto. * apply H1; red;apply Hq_prop. red;intros;simpl;red;simpl; intros x1 y1 Hx1; apply H. rewrite Hzt, Hx1;reflexivity. reflexivity. intros x1 y1 Hx1 ;apply H. rewrite Hx1;reflexivity. reflexivity. intros x1 y1 Hx1;simpl;red;simpl. apply H. rewrite Hx1, Hzt; reflexivity. assumption. assumption. - specialize (Hbr H0 a); rewrite Hbr. specialize (Hq (fun y : A => z <--- y times a ^ r; k z (a ^ b))). assert ( Fkont_proper M (fun y : A => z <--- y times a ^ r; k z (a ^ b))). + red; intros x y Hxy; red; simpl. apply H. rewrite Hxy;reflexivity. reflexivity. + rewrite (Hq H1);simpl;apply H. monoid_simpl M. rewrite (power_of_power M a b q). rewrite (Nat.mul_comm q b). rewrite power_of_plus; reflexivity. 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)