proposition: Lemma develop_det (p q r: Plane): det p q r = xcoord r * (ycoord p - ycoord q) - ycoord r * (xcoord p - xcoord q) + xcoord p * ycoord q - ycoord p * xcoord q.
proof: Proof. rewrite /det (expand_det_col (det_mx p q r) (lift ord0 (lift ord0 (@ord0 0)))). rewrite !big_ord_recl big_ord0 !mxE/= -!addrA; congr (_ * _ + _). by rewrite /cofactor !det2 !mxE /get_coord/get_pt /=; ring. by rewrite -mulrN; congr (_ * _ + _); rewrite /cofactor !det2 !mxE /get_coord/get_pt /=; ring. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)