proposition: Lemma det_scalar_productE (p q r: Plane): det p q r = scalar_product (q-p) (rotate (r-p)).
proof: Proof. by rewrite develop_det /scalar_product /=; ring. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)