proposition: Theorem Field_simplify_aux_ok l fe1 fe2 den : FEeval l fe1 == FEeval l fe2 -> split (denum (Fnorm fe1)) (denum (Fnorm fe2)) = den -> PCond l (condition (Fnorm fe1) ++ condition (Fnorm fe2)) -> (num (Fnorm fe1) * right den) @ l == (num (Fnorm fe2) * left den) @ l.
proof: Proof. rewrite PCond_app; intros Hfe Hden (Hc1,Hc2); simpl. assert (Hc1' := Pcond_Fnorm _ _ Hc1). assert (Hc2' := Pcond_Fnorm _ _ Hc2). set (N1 := num (Fnorm fe1)) in *. set (N2 := num (Fnorm fe2)) in *. set (D1 := denum (Fnorm fe1)) in *. set (D2 := denum (Fnorm fe2)) in *. assert (~ (common den) @ l == 0). { intro H. apply Hc1'. rewrite (split_ok_l D1 D2 l). rewrite Hden. simpl. ring [H]. } apply (@rmul_reg_l ((common den) @ l)); trivial. rewrite !(rmul_comm ((common den) @ l)), <- !rmul_assoc. change (N1@l * (right den * common den) @ l == N2@l * (left den * common den) @ l). rewrite <- Hden, <- split_ok_l, <- split_ok_r. apply (@rmul_reg_l (/ D2@l)). { apply rinv_nz; trivial. } rewrite (rmul_comm (/ D2 @ l)), <- !rmul_assoc. rewrite <- rdiv_def, rdiv_r_r, rmul_1_r by trivial. apply (@rmul_reg_l (/ (D1@l))). { apply rinv_nz; trivial. } rewrite !(rmul_comm (/ D1@l)), <- !rmul_assoc. rewrite <- !rdiv_def, rdiv_r_r, rmul_1_r by trivial. rewrite (rmul_comm (/ D2@l)), <- rdiv_def. unfold N1,N2,D1,D2; rewrite <- !Fnorm_FEeval_PEeval; trivial. Qed.
imports: ZArith_base