proposition: Theorem Fnorm_crossproduct l fe1 fe2 : let nfe1 := Fnorm fe1 in let nfe2 := Fnorm fe2 in (num nfe1 * denum nfe2) @ l == (num nfe2 * denum nfe1) @ l -> PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2.
proof: Proof. simpl. rewrite PCond_app. intros Hcrossprod (Hc1,Hc2). rewrite !Fnorm_FEeval_PEeval; trivial. apply cross_product_eq; trivial; apply Pcond_Fnorm; trivial. Qed.
imports: ZArith_base