proposition: Lemma FF_mult_corr_F : forall (e f:expr) (x y:F), II e x -> II f y -> II (FF_mult e f) (x[*]y).
proof: Proof. cut (forall (e1 e2 f1 f2:expr) (x y:F), II (expr_div e1 e2) x -> II (expr_div f1 f2) y -> II (expr_div (PP_mult e1 f1) (PP_mult e2 f2)) (x[*]y)). cut (forall (e f:expr) (x y:F), II e x -> II f y -> II (expr_mult e f) (x[*]y)). intros H H0 e f. elim e; elim f; intros; simpl in |- *; auto. intros. apply interpF_mult with x y; 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 (y0[*]y1[#][0]). intro H13. apply interpF_div with (x0[*]x1) (y0[*]y1) H13. Step_final ((x0[/] y0[//]nzy)[*](x1[/] y1[//]nzy0)). apply PP_mult_corr_F; auto. apply PP_mult_corr_F; auto. apply mult_resp_ap_zero; auto. Qed.
imports: CoRN.algebra.CFields CoRN.tactics.AlgReflection