fact: Axiom determinant_def : forall (A B C D : PO) (x y x' y' : R), vec A B = add_PP (mult_PP x (vec O I)) (mult_PP y (vec O J)) -> vec C D = add_PP (mult_PP x' (vec O I)) (mult_PP y' (vec O J)) -> det (vec A B) (vec C D) = x * y' + - (y * x').