proposition: Lemma FF_div_corr_F : forall (e f:expr) (x y:F) (nzy:y[#][0]), II e x -> II f y -> II (FF_div e f) (x[/]y[//]nzy).
proof: Proof. cut (forall (e1 e2 f1 f2:expr) (x y:F) (nzy:y[#][0]), II (expr_div e1 e2) x -> II (expr_div f1 f2) y -> II (expr_div (PP_mult e1 f2) (PP_mult e2 f1)) (x[/]y[//]nzy)). cut (forall (e f:expr) (x y:F) (nzy:y[#][0]), II e x -> II f y -> II (expr_div e f) (x[/]y[//]nzy)). intros H H0 e f. elim e; elim f; intros; simpl in |- *; auto. intros. apply interpF_div with x y nzy; algebra. intros. inversion X. try (rewrite H in X1; rewrite H1 in X2; rewrite H0 in H2). inversion X0. try (rewrite H3 in X3; rewrite H5 in X4; rewrite H4 in H6). cut (x1[#][0]). intro nzx1. cut (y0[*]x1[#][0]). intro H13. cut ((x1[/]y1[//]nzy1)[#][0]). intro H14. apply interpF_div with (x0[*]y1) (y0[*]x1) H13. astepl ((y1[*]x0)[/]y0[*]x1[//]H13). astepl (((y1[*]x0)[/]y0[//]nzy0)[/]x1[//]nzx1). astepl ((y1[*](x0[/]y0[//]nzy0))[/]x1[//]nzx1). astepl (((x0[/]y0[//]nzy0)[*]y1)[/]x1[//]nzx1). Step_final ((x0[/]y0[//]nzy0)[/]x1[/]y1[//]nzy1[//]H14). apply PP_mult_corr_F; auto. apply PP_mult_corr_F; auto. apply div_resp_ap_zero_rev; auto. apply mult_resp_ap_zero; auto. apply div_resp_ap_zero with y1 nzy1. astepl y. auto. Qed.
imports: CoRN.algebra.CFields CoRN.tactics.AlgReflection